MeasureTheory.MeasureSpace.StronglyMeasurable

このファイルでは強可測の定義を行います.

コード元 MeasureTheory.MeasurableSpace.StronglyMeasurable

variable {α β γ ι : Type*} [Countable ι]

namespace MeasureTheory

local infixr:25 " →ₛ " => SimpleFunc

section Definitions

variable [TopologicalSpace β]

/-- A function is `StronglyMeasurable` if it is the limit of simple functions. -/
def StronglyMeasurable [MeasurableSpace α] (f : α → β) : Prop :=
  ∃ fs : ℕ → α →ₛ β, ∀ x, Tendsto (fun n => fs n x) atTop (nhds (f x))

ある単関数列fsが存在して, すべてのxでf xの近傍の極限に, 単関数の値fs n xが収束することを要求しています.

/-- The notation for StronglyMeasurable giving the measurable space instance explicitly. -/
scoped notation "StronglyMeasurable[" m "]" => @MeasureTheory.StronglyMeasurable _ _ _ m

mが強可測であることはStronglyMeasurable[m]と略記できます.