# 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 : } [] {f : αβ} {μ : } [] :
theorem aemeasurable_of_subsingleton_codomain {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } [] :
@[simp]
theorem aemeasurable_zero_measure {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} :
theorem aemeasurable_id'' {α : Type u_2} {m0 : } (μ : ) {m : } (hm : m m0) :
theorem aemeasurable_of_map_neZero {α : Type u_2} {β : Type u_3} {m0 : } {mβ : } {μ : } {f : αβ} (h : ) :
theorem AEMeasurable.mono_ac {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {ν : } (hf : ) (hμν : μ.AbsolutelyContinuous ν) :
theorem AEMeasurable.mono_measure {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {ν : } (h : ) (h' : ν μ) :
theorem AEMeasurable.mono_set {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {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 : } [] {f : αβ} {μ : } {ν : } (h : ) (h' : ν.AbsolutelyContinuous μ) :
theorem AEMeasurable.ae_mem_imp_eq_mk {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {s : Set α} (h : AEMeasurable f (μ.restrict s)) :
∀ᵐ (x : α) ∂μ, x sf x =
theorem AEMeasurable.ae_inf_principal_eq_mk {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {s : Set α} (h : AEMeasurable f (μ.restrict s)) :
(μ.ae ).EventuallyEq f ()
theorem AEMeasurable.sum_measure {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} [] {μ : } (h : ∀ (i : ι), AEMeasurable f (μ i)) :
@[simp]
theorem aemeasurable_sum_measure_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} [] {μ : } :
∀ (i : ι), AEMeasurable f (μ i)
@[simp]
theorem aemeasurable_add_measure_iff {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {ν : } :
AEMeasurable f (μ + ν)
theorem AEMeasurable.add_measure {α : Type u_2} {β : Type u_3} {m0 : } [] {μ : } {ν : } {f : αβ} (hμ : ) (hν : ) :
AEMeasurable f (μ + ν)
theorem AEMeasurable.iUnion {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } [] {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 : } [] {f : αβ} {μ : } [] {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 : } [] {f : αβ} {μ : } {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 : } [] {f : αβ} {μ : } [] (h : ) (c : R) :
AEMeasurable f (c μ)
theorem AEMeasurable.comp_aemeasurable {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : } [] [] {μ : } {f : αδ} {g : δβ} (hg : ) (hf : ) :
AEMeasurable (g f) μ
theorem AEMeasurable.comp_measurable {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : } [] [] {μ : } {f : αδ} {g : δβ} (hg : ) (hf : ) :
AEMeasurable (g f) μ
theorem AEMeasurable.comp_quasiMeasurePreserving {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : } [] [] {μ : } {ν : } {f : αδ} {g : δβ} (hg : ) (hf : ) :
AEMeasurable (g f) μ
theorem AEMeasurable.map_map_of_aemeasurable {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : } [] [] {μ : } {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem AEMeasurable.prod_mk {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : } [] [] {μ : } {f : αβ} {g : αγ} (hf : ) (hg : ) :
AEMeasurable (fun (x : α) => (f x, g x)) μ
theorem AEMeasurable.exists_ae_eq_range_subset {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } (H : ) {t : Set β} (ht : ∀ᵐ (x : α) ∂μ, f x t) (h₀ : t.Nonempty) :
∃ (g : αβ), t μ.ae.EventuallyEq f g
theorem AEMeasurable.exists_measurable_nonneg {α : Type u_2} {m0 : } {μ : } {β : Type u_7} [] [Zero β] {mβ : } {f : αβ} (hf : ) (f_nn : ∀ᵐ (t : α) ∂μ, 0 f t) :
∃ (g : αβ), 0 g μ.ae.EventuallyEq f g
theorem AEMeasurable.subtype_mk {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } (h : ) {s : Set β} {hfs : ∀ (x : α), f x s} :
theorem aemeasurable_const' {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } (h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y) :
theorem aemeasurable_uIoc_iff {α : Type u_2} {β : Type u_3} {m0 : } [] {μ : } [] {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 : } [] {f : αβ} {μ : } [μ.IsComplete] :
theorem MeasurableEmbedding.aemeasurable_map_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : } [] [] {f : αβ} {μ : } {g : βγ} (hf : ) :
AEMeasurable (g f) μ
theorem MeasurableEmbedding.aemeasurable_comp_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : } [] [] {f : αβ} {g : βγ} (hg : ) {μ : } :
AEMeasurable (g f) μ
theorem aemeasurable_restrict_iff_comap_subtype {α : Type u_2} {β : Type u_3} {m0 : } [] {s : Set α} (hs : ) {μ : } {f : αβ} :
AEMeasurable f (μ.restrict s) AEMeasurable (f Subtype.val) (MeasureTheory.Measure.comap Subtype.val μ)
theorem aemeasurable_zero {α : Type u_2} {β : Type u_3} {m0 : } [] {μ : } [Zero β] :
AEMeasurable (fun (x : α) => 0) μ
theorem aemeasurable_one {α : Type u_2} {β : Type u_3} {m0 : } [] {μ : } [One β] :
AEMeasurable (fun (x : α) => 1) μ
@[simp]
theorem aemeasurable_smul_measure_iff {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {c : ENNReal} (hc : c 0) :
AEMeasurable f (c μ)
theorem aemeasurable_of_aemeasurable_trim {β : Type u_3} [] {α : Type u_7} {m : } {m0 : } {μ : } (hm : m m0) {f : αβ} (hf : AEMeasurable f (μ.trim hm)) :
theorem aemeasurable_restrict_of_measurable_subtype {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } {s : Set α} (hs : ) (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 : } [] [] {μ : } (e : α ≃ᵐ β) {f : βγ} :
AEMeasurable f () AEMeasurable (f e) μ
theorem AEMeasurable.restrict {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } (hfm : ) {s : Set α} :
AEMeasurable f (μ.restrict s)
theorem aemeasurable_Ioi_of_forall_Ioc {α : Type u_2} {m0 : } {μ : } {β : Type u_7} {mβ : } [] [Filter.atTop.IsCountablyGenerated] {x : α} {g : αβ} (g_meas : t > x, AEMeasurable g (μ.restrict (Set.Ioc x t))) :
AEMeasurable g (μ.restrict ())
theorem aemeasurable_indicator_iff {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } [Zero β] {s : Set α} (hs : ) :
AEMeasurable (s.indicator f) μ AEMeasurable f (μ.restrict s)
theorem aemeasurable_indicator_iff₀ {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } [Zero β] {s : Set α} (hs : ) :
AEMeasurable (s.indicator f) μ AEMeasurable f (μ.restrict s)
theorem aemeasurable_indicator_const_iff {α : Type u_2} {β : Type u_3} {m0 : } [] {μ : } [Zero β] {s : Set α} (b : β) [] :
AEMeasurable (s.indicator fun (x : α) => b) μ

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 : } [] {f : αβ} {μ : } [Zero β] (hfm : ) {s : Set α} (hs : ) :
AEMeasurable (s.indicator f) μ
theorem AEMeasurable.indicator₀ {α : Type u_2} {β : Type u_3} {m0 : } [] {f : αβ} {μ : } [Zero β] (hfm : ) {s : Set α} (hs : ) :
AEMeasurable (s.indicator f) μ
theorem MeasureTheory.Measure.restrict_map_of_aemeasurable {α : Type u_2} {δ : Type u_5} {m0 : } [] {μ : } {f : αδ} (hf : ) {s : Set δ} (hs : ) :
.restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
theorem MeasureTheory.Measure.map_mono_of_aemeasurable {α : Type u_2} {δ : Type u_5} {m0 : } [] {μ : } {ν : } {f : αδ} (h : μ ν) (hf : ) :
theorem MeasureTheory.NullMeasurable.aemeasurable {α : Type u_2} {β : Type u_3} {m0 : } [] {μ : } {f : αβ} (h : ) :

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 : } [] {μ : } {f : αβ} {t : Set β} (h : ) (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.

theorem MeasureTheory.Measure.map_sum {α : Type u_2} {β : Type u_3} {m0 : } [] {ι : Type u_7} {m : } {f : αβ} (hf : ) :
= MeasureTheory.Measure.sum fun (i : ι) =>
instance MeasureTheory.Measure.instSFiniteMap {α : Type u_2} {β : Type u_3} {m0 : } [] (μ : ) (f : αβ) :
Equations
• =