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)
:
AEMeasurable id
theorem
aemeasurable_of_map_neZero
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{mβ : 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μν : MeasureTheory.Measure.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)
:
theorem
AEMeasurable.mono'
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : AEMeasurable f)
(h' : MeasureTheory.Measure.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)
:
∀ᵐ (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)
:
theorem
AEMeasurable.sum_measure
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
[Countable ι]
{μ : ι → MeasureTheory.Measure α}
(h : ∀ (i : ι), AEMeasurable f)
:
@[simp]
theorem
aemeasurable_sum_measure_iff
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
[Countable ι]
{μ : ι → MeasureTheory.Measure α}
:
AEMeasurable f ↔ ∀ (i : ι), AEMeasurable f
@[simp]
theorem
aemeasurable_add_measure_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
theorem
AEMeasurable.add_measure
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : α → β}
(hμ : AEMeasurable f)
(hν : 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)
:
@[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 ↔ ∀ (i : ι), AEMeasurable f
@[simp]
theorem
aemeasurable_union_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
:
AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
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)
:
theorem
AEMeasurable.comp_aemeasurable
{α : Type u_2}
{β : Type u_3}
{δ : Type u_5}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{f : α → δ}
{g : δ → β}
(hg : AEMeasurable g)
(hf : AEMeasurable f)
:
AEMeasurable (g ∘ f)
theorem
AEMeasurable.comp_measurable
{α : Type u_2}
{β : Type u_3}
{δ : Type u_5}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{f : α → δ}
{g : δ → β}
(hg : AEMeasurable g)
(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)
(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₀ : Set.Nonempty t)
:
∃ (g : α → β), Measurable g ∧ Set.range g ⊆ t ∧ f =ᶠ[MeasureTheory.Measure.ae μ] 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 =ᶠ[MeasureTheory.Measure.ae μ] 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}
:
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)
:
theorem
aemeasurable_uIoc_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[LinearOrder α]
{f : α → β}
{a : α}
{b : α}
:
AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
theorem
aemeasurable_iff_measurable
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
[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 ↔ 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 ↔ AEMeasurable (f ∘ 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)
:
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)
:
theorem
aemeasurable_map_equiv_iff
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
(e : α ≃ᵐ β)
{f : β → γ}
:
AEMeasurable f ↔ AEMeasurable (f ∘ ⇑e)
theorem
AEMeasurable.restrict
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
(hfm : AEMeasurable f)
{s : Set α}
:
theorem
aemeasurable_Ioi_of_forall_Ioc
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
{mβ : MeasurableSpace β}
[LinearOrder α]
[Filter.IsCountablyGenerated Filter.atTop]
{x : α}
{g : α → β}
(g_meas : ∀ t > x, AEMeasurable g)
:
theorem
aemeasurable_indicator_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
[Zero β]
{s : Set α}
(hs : MeasurableSet s)
:
AEMeasurable (Set.indicator s f) ↔ AEMeasurable f
theorem
aemeasurable_indicator_iff₀
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
[Zero β]
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s)
:
AEMeasurable (Set.indicator s f) ↔ AEMeasurable f
theorem
aemeasurable_indicator_const_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[Zero β]
{s : Set α}
[MeasurableSingletonClass β]
(b : β)
[NeZero b]
:
AEMeasurable (Set.indicator s 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 (Set.indicator s 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 (Set.indicator s 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)
:
theorem
MeasureTheory.Measure.map_mono_of_aemeasurable
{α : Type u_2}
{δ : Type u_5}
{m0 : MeasurableSpace α}
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{ν : 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)
:
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.
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.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 μ]
:
Equations
- (_ : MeasureTheory.SFinite (MeasureTheory.Measure.map f μ)) = (_ : MeasureTheory.SFinite (MeasureTheory.Measure.map f μ))