# 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.

source
theorem Subsingleton.aemeasurable {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} [Subsingleton α] :
AEMeasurable f μ
source
theorem aemeasurable_of_subsingleton_codomain {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} [Subsingleton β] :
AEMeasurable f μ
source
@[simp]
theorem aemeasurable_zero_measure {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} :
AEMeasurable f 0
source
theorem aemeasurable_id'' {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {m : MeasurableSpace α} (hm : m ≤ m0) :
AEMeasurable id μ
source
theorem aemeasurable_of_map_neZero {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (h : NeZero (MeasureTheory.Measure.map f μ)) :
AEMeasurable f μ
source
theorem AEMeasurable.mono_ac {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ ν : MeasureTheory.Measure α} (hf : AEMeasurable f ν) (hμν : μ.AbsolutelyContinuous ν) :
AEMeasurable f μ
source
theorem AEMeasurable.mono_measure {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ ν : MeasureTheory.Measure α} (h : AEMeasurable f μ) (h' : ν ≤ μ) :
AEMeasurable f ν
source
theorem AEMeasurable.mono_set {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} {s t : Set α} (h : s ⊆ t) (ht : AEMeasurable f (μ.restrict t)) :
AEMeasurable f (μ.restrict s)
source
theorem AEMeasurable.mono' {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ ν : MeasureTheory.Measure α} (h : AEMeasurable f μ) (h' : ν.AbsolutelyContinuous μ) :
AEMeasurable f ν
source
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 ∈ s → f x = mk f h x
source
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)) :
f =ᶠ[MeasureTheory.ae μ ⊓ Filter.principal s] mk f h
source
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)) :
AEMeasurable f (MeasureTheory.Measure.sum μ)
source
@[simp]
theorem aemeasurable_sum_measure_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} [Countable ι] {μ : ι → MeasureTheory.Measure α} :
AEMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), AEMeasurable f (μ i)
source
@[simp]
theorem aemeasurable_add_measure_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ ν : MeasureTheory.Measure α} :
AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
source
theorem AEMeasurable.add_measure {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ ν : MeasureTheory.Measure α} {f : α → β} (hμ : AEMeasurable f μ) (hν : AEMeasurable f ν) :
AEMeasurable f (μ + ν)
source
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))
source
@[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))
source
@[simp]
theorem aemeasurable_union_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} {s t : Set α} :
AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)
source
theorem AEMeasurable.smul_measure {α : Type u_2} {β : Type u_3} {R : Type u_6} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : AEMeasurable f μ) (c : R) :
AEMeasurable f (c • μ)
source
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) μ
source
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)) μ
source
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) μ
source
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) μ
source
theorem AEMeasurable.map_map_of_aemeasurable {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) :
MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
source
theorem AEMeasurable.fst {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : α → β × γ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => (f x).1) μ
source
theorem AEMeasurable.snd {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : α → β × γ} (hf : AEMeasurable f μ) :
AEMeasurable (fun (x : α) => (f x).2) μ
source
theorem AEMeasurable.prodMk {α : 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)) μ
source
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
source
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
source
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} :
AEMeasurable (Set.codRestrict f s hfs) μ
source
theorem aemeasurable_const' {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y) :
AEMeasurable f μ
source
theorem aemeasurable_uIoc_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [LinearOrder α] {f : α → β} {a b : α} :
AEMeasurable f (μ.restrict (Set.uIoc a b)) ↔ AEMeasurable f (μ.restrict (Set.Ioc a b)) ∧ AEMeasurable f (μ.restrict (Set.Ioc b a))
source
theorem aemeasurable_iff_measurable {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} [μ.IsComplete] :
AEMeasurable f μ ↔ Measurable f
source
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) :
AEMeasurable g (MeasureTheory.Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ
source
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 α} :
AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ
source
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 μ)
source
theorem aemeasurable_one {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [One β] :
AEMeasurable (fun (x : α) => 1) μ
source
theorem aemeasurable_zero {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [Zero β] :
AEMeasurable (fun (x : α) => 0) μ
source
@[simp]
theorem aemeasurable_smul_measure_iff {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} {c : ENNReal} (hc : c ≠ 0) :
AEMeasurable f (c • μ) ↔ AEMeasurable f μ
source
theorem aemeasurable_of_aemeasurable_trim {β : Type u_3} [MeasurableSpace β] {α : Type u_7} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → β} (hf : AEMeasurable f (μ.trim hm)) :
AEMeasurable f μ
source
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)
source
theorem aemeasurable_map_equiv_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) {f : β → γ} :
AEMeasurable f (MeasureTheory.Measure.map (⇑e) μ) ↔ AEMeasurable (f ∘ ⇑e) μ
source
theorem AEMeasurable.restrict {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (hfm : AEMeasurable f μ) {s : Set α} :
AEMeasurable f (μ.restrict s)
source
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))
source
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)
source
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)
source
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.

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

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

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

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.

source
theorem MeasureTheory.Measure.map_sum {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {ι : Type u_7} {m : ι → Measure α} {f : α → β} (hf : AEMeasurable f (sum m)) :
map f (sum m) = sum fun (i : ι) => map f (m i)
source
instance MeasureTheory.Measure.instSFiniteMap {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : Measure α) (f : α → β) [SFinite μ] :
SFinite (map f μ)