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 α]
:
AEMeasurable f μ
theorem
aemeasurable_of_subsingleton_codomain
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
[Subsingleton β]
:
AEMeasurable f μ
@[simp]
theorem
aemeasurable_zero_measure
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
:
AEMeasurable f 0
theorem
aemeasurable_id''
{α : Type u_2}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{m : MeasurableSpace α}
(hm : m ≤ m0)
:
AEMeasurable id μ
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 μ
theorem
AEMeasurable.mono_ac
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ ν : MeasureTheory.Measure α}
(hf : AEMeasurable f ν)
(hμν : μ.AbsolutelyContinuous ν)
:
AEMeasurable f μ
theorem
AEMeasurable.mono_measure
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ ν : MeasureTheory.Measure α}
(h : AEMeasurable f μ)
(h' : ν ≤ μ)
:
AEMeasurable f ν
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)
theorem
AEMeasurable.mono'
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ ν : MeasureTheory.Measure α}
(h : AEMeasurable f μ)
(h' : ν.AbsolutelyContinuous μ)
:
AEMeasurable f ν
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 = 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))
:
f =ᶠ[MeasureTheory.ae μ ⊓ Filter.principal s] AEMeasurable.mk f h
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 α}
:
AEMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), AEMeasurable f (μ i)
@[simp]
theorem
aemeasurable_add_measure_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ ν : MeasureTheory.Measure α}
:
AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
theorem
AEMeasurable.add_measure
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ ν : 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 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.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) μ
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)
:
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)
:
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) μ
theorem
aemeasurable_const'
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y)
:
AEMeasurable f μ
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]
:
AEMeasurable f μ ↔ Measurable f
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) μ
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 μ
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_one
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[One β]
:
AEMeasurable (fun (x : α) => 1) μ
theorem
aemeasurable_zero
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[Zero β]
:
AEMeasurable (fun (x : α) => 0) μ
@[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 μ
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 μ
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 : β → γ}
:
AEMeasurable f (MeasureTheory.Measure.map (⇑e) μ) ↔ AEMeasurable (f ∘ ⇑e) μ
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))
theorem
MeasureTheory.Measure.map_mono_of_aemeasurable
{α : Type u_2}
{δ : Type u_5}
{m0 : MeasurableSpace α}
[MeasurableSpace δ]
{μ ν : MeasureTheory.Measure α}
{f : α → δ}
(h : μ ≤ ν)
(hf : AEMeasurable f ν)
:
theorem
MeasureTheory.NullMeasurable.aemeasurable
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
[hc : MeasurableSpace.CountablyGenerated β]
(h : MeasureTheory.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.
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)
:
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.
theorem
MeasureTheory.Measure.map_sum
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{ι : Type u_7}
{m : ι → MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f (MeasureTheory.Measure.sum m))
:
MeasureTheory.Measure.map f (MeasureTheory.Measure.sum m) = MeasureTheory.Measure.sum fun (i : ι) => MeasureTheory.Measure.map f (m i)
instance
MeasureTheory.Measure.instSFiniteMap
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(f : α → β)
[MeasureTheory.SFinite μ]
: