Documentation

Mathlib.MeasureTheory.Measure.AEMeasurable

Almost everywhere measurable functions #

A function is almost everywhere measurable if it coincides almost everywhere with a measurable function. This property, called AEMeasurable f μ, is defined in the file MeasureSpaceDef. We discuss several of its properties that are analogous to properties of measurable functions.

theorem Subsingleton.aemeasurable {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Subsingleton α] :
theorem aemeasurable_of_subsingleton_codomain {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Subsingleton β] :
@[simp]
theorem aemeasurable_zero_measure {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} :
theorem aemeasurable_id'' {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {m : MeasurableSpace α} (hm : m m0) :
theorem aemeasurable_of_map_neZero {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (h : NeZero (MeasureTheory.Measure.map f μ)) :
theorem AEMeasurable.mono_ac {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (hf : AEMeasurable f ν) (hμν : μ.AbsolutelyContinuous ν) :
theorem AEMeasurable.mono_measure {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : AEMeasurable f μ) (h' : ν μ) :
theorem AEMeasurable.mono_set {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s t) (ht : AEMeasurable f (μ.restrict t)) :
AEMeasurable f (μ.restrict s)
theorem AEMeasurable.mono' {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : AEMeasurable f μ) (h' : ν.AbsolutelyContinuous μ) :
theorem AEMeasurable.ae_mem_imp_eq_mk {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {s : Set α} (h : AEMeasurable f (μ.restrict s)) :
∀ᵐ (x : α) ∂μ, x sf x = AEMeasurable.mk f h x
theorem AEMeasurable.ae_inf_principal_eq_mk {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {s : Set α} (h : AEMeasurable f (μ.restrict s)) :
theorem AEMeasurable.sum_measure {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} [Countable ι] {μ : ιMeasureTheory.Measure α} (h : ∀ (i : ι), AEMeasurable f (μ i)) :
@[simp]
theorem aemeasurable_sum_measure_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} [Countable ι] {μ : ιMeasureTheory.Measure α} :
@[simp]
theorem aemeasurable_add_measure_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
theorem AEMeasurable.add_measure {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : αβ} (hμ : AEMeasurable f μ) (hν : AEMeasurable f ν) :
AEMeasurable f (μ + ν)
theorem AEMeasurable.iUnion {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} (h : ∀ (i : ι), AEMeasurable f (μ.restrict (s i))) :
AEMeasurable f (μ.restrict (⋃ (i : ι), s i))
@[simp]
theorem aemeasurable_iUnion_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} :
AEMeasurable f (μ.restrict (⋃ (i : ι), s i)) ∀ (i : ι), AEMeasurable f (μ.restrict (s i))
@[simp]
theorem aemeasurable_union_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} :
AEMeasurable f (μ.restrict (s t)) AEMeasurable f (μ.restrict s) AEMeasurable f (μ.restrict t)
theorem AEMeasurable.smul_measure {α : Type u_2} {β : Type u_3} {R : Type u_6} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : AEMeasurable f μ) (c : R) :
AEMeasurable f (c μ)
theorem AEMeasurable.comp_aemeasurable {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : αδ} {g : δβ} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) :
AEMeasurable (g f) μ
theorem AEMeasurable.comp_aemeasurable' {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : αδ} {g : δβ} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => g (f x)) μ
theorem AEMeasurable.comp_measurable {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : αδ} {g : δβ} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : Measurable f) :
AEMeasurable (g f) μ
theorem AEMeasurable.comp_quasiMeasurePreserving {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure δ} {f : αδ} {g : δβ} (hg : AEMeasurable g ν) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν) :
AEMeasurable (g f) μ
theorem AEMeasurable.prod_mk {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : αβ} {g : αγ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
AEMeasurable (fun (x : α) => (f x, g x)) μ
theorem AEMeasurable.exists_ae_eq_range_subset {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} (H : AEMeasurable f μ) {t : Set β} (ht : ∀ᵐ (x : α) ∂μ, f x t) (h₀ : t.Nonempty) :
∃ (g : αβ), Measurable g Set.range g t f =ᵐ[μ] g
theorem AEMeasurable.exists_measurable_nonneg {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [Preorder β] [Zero β] {mβ : MeasurableSpace β} {f : αβ} (hf : AEMeasurable f μ) (f_nn : ∀ᵐ (t : α) ∂μ, 0 f t) :
∃ (g : αβ), Measurable g 0 g f =ᵐ[μ] g
theorem AEMeasurable.subtype_mk {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} (h : AEMeasurable f μ) {s : Set β} {hfs : ∀ (x : α), f x s} :
theorem aemeasurable_const' {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} (h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y) :
theorem aemeasurable_uIoc_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [LinearOrder α] {f : αβ} {a : α} {b : α} :
AEMeasurable f (μ.restrict (Ι a b)) AEMeasurable f (μ.restrict (Set.Ioc a b)) AEMeasurable f (μ.restrict (Set.Ioc b a))
theorem aemeasurable_iff_measurable {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [μ.IsComplete] :
theorem MeasurableEmbedding.aemeasurable_map_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {μ : MeasureTheory.Measure α} {g : βγ} (hf : MeasurableEmbedding f) :
theorem MeasurableEmbedding.aemeasurable_comp_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {g : βγ} (hg : MeasurableEmbedding g) {μ : MeasureTheory.Measure α} :
theorem aemeasurable_restrict_iff_comap_subtype {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {s : Set α} (hs : MeasurableSet s) {μ : MeasureTheory.Measure α} {f : αβ} :
AEMeasurable f (μ.restrict s) AEMeasurable (f Subtype.val) (MeasureTheory.Measure.comap Subtype.val μ)
theorem aemeasurable_zero {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [Zero β] :
AEMeasurable (fun (x : α) => 0) μ
theorem aemeasurable_one {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [One β] :
AEMeasurable (fun (x : α) => 1) μ
@[simp]
theorem aemeasurable_smul_measure_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {c : ENNReal} (hc : c 0) :
theorem aemeasurable_of_aemeasurable_trim {β : Type u_3} [MeasurableSpace β] {α : Type u_7} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) {f : αβ} (hf : AEMeasurable f (μ.trim hm)) :
theorem aemeasurable_restrict_of_measurable_subtype {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hf : Measurable fun (x : s) => f x) :
AEMeasurable f (μ.restrict s)
theorem aemeasurable_map_equiv_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) {f : βγ} :
theorem AEMeasurable.restrict {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} (hfm : AEMeasurable f μ) {s : Set α} :
AEMeasurable f (μ.restrict s)
theorem aemeasurable_Ioi_of_forall_Ioc {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {mβ : MeasurableSpace β} [LinearOrder α] [Filter.atTop.IsCountablyGenerated] {x : α} {g : αβ} (g_meas : t > x, AEMeasurable g (μ.restrict (Set.Ioc x t))) :
AEMeasurable g (μ.restrict (Set.Ioi x))
theorem aemeasurable_indicator_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Zero β] {s : Set α} (hs : MeasurableSet s) :
AEMeasurable (s.indicator f) μ AEMeasurable f (μ.restrict s)
theorem aemeasurable_indicator_iff₀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Zero β] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) :
AEMeasurable (s.indicator f) μ AEMeasurable f (μ.restrict s)
theorem aemeasurable_indicator_const_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [Zero β] {s : Set α} [MeasurableSingletonClass β] (b : β) [NeZero b] :
AEMeasurable (s.indicator fun (x : α) => b) μ MeasureTheory.NullMeasurableSet s μ

A characterization of the a.e.-measurability of the indicator function which takes a constant value b on a set A and 0 elsewhere.

theorem AEMeasurable.indicator {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Zero β] (hfm : AEMeasurable f μ) {s : Set α} (hs : MeasurableSet s) :
AEMeasurable (s.indicator f) μ
theorem AEMeasurable.indicator₀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} [Zero β] (hfm : AEMeasurable f μ) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) :
AEMeasurable (s.indicator f) μ
theorem MeasureTheory.Measure.restrict_map_of_aemeasurable {α : Type u_2} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : αδ} (hf : AEMeasurable f μ) {s : Set δ} (hs : MeasurableSet s) :
(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))

If the σ-algebra of the codomain of a null measurable function is countably generated, then the function is a.e.-measurable.

theorem MeasureTheory.NullMeasurable.aemeasurable_of_aerange {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} {t : Set β} [MeasurableSpace.CountablyGenerated t] (h : MeasureTheory.NullMeasurable f μ) (hft : ∀ᵐ (x : α) ∂μ, f x t) :

Let f : α → β be a null measurable function such that a.e. all values of f belong to a set t such that the restriction of the σ-algebra in the codomain to t is countably generated, then f is a.e.-measurable.