Almost everywhere measurable functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function. This property, called ae_measurable f μ, is defined in the file measure_space_def.
We discuss several of its properties that are analogous to properties of measurable functions.
@[measurability]
theorem
subsingleton.ae_measurable
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[subsingleton α] :
ae_measurable f μ
@[measurability]
theorem
ae_measurable_of_subsingleton_codomain
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[subsingleton β] :
ae_measurable f μ
@[simp, measurability]
theorem
ae_measurable_zero_measure
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β} :
ae_measurable f 0
theorem
ae_measurable.mono_measure
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ ν : measure_theory.measure α}
(h : ae_measurable f μ)
(h' : ν ≤ μ) :
ae_measurable f ν
theorem
ae_measurable.mono_set
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{s t : set α}
(h : s ⊆ t)
(ht : ae_measurable f (μ.restrict t)) :
ae_measurable f (μ.restrict s)
@[protected]
theorem
ae_measurable.mono'
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ ν : measure_theory.measure α}
(h : ae_measurable f μ)
(h' : ν.absolutely_continuous μ) :
ae_measurable f ν
theorem
ae_measurable.ae_mem_imp_eq_mk
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{s : set α}
(h : ae_measurable f (μ.restrict s)) :
theorem
ae_measurable.ae_inf_principal_eq_mk
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{s : set α}
(h : ae_measurable f (μ.restrict s)) :
f =ᶠ[μ.ae ⊓ filter.principal s] ae_measurable.mk f h
@[measurability]
theorem
ae_measurable.sum_measure
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
[countable ι]
{μ : ι → measure_theory.measure α}
(h : ∀ (i : ι), ae_measurable f (μ i)) :
@[simp]
theorem
ae_measurable_sum_measure_iff
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
[countable ι]
{μ : ι → measure_theory.measure α} :
ae_measurable f (measure_theory.measure.sum μ) ↔ ∀ (i : ι), ae_measurable f (μ i)
@[simp]
theorem
ae_measurable_add_measure_iff
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ ν : measure_theory.measure α} :
ae_measurable f (μ + ν) ↔ ae_measurable f μ ∧ ae_measurable f ν
@[measurability]
theorem
ae_measurable.add_measure
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{μ ν : measure_theory.measure α}
{f : α → β}
(hμ : ae_measurable f μ)
(hν : ae_measurable f ν) :
ae_measurable f (μ + ν)
@[protected, measurability]
theorem
ae_measurable.Union
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(h : ∀ (i : ι), ae_measurable f (μ.restrict (s i))) :
ae_measurable f (μ.restrict (⋃ (i : ι), s i))
@[simp]
theorem
ae_measurable_Union_iff
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α} :
ae_measurable f (μ.restrict (⋃ (i : ι), s i)) ↔ ∀ (i : ι), ae_measurable f (μ.restrict (s i))
@[simp]
theorem
ae_measurable_union_iff
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{s t : set α} :
ae_measurable f (μ.restrict (s ∪ t)) ↔ ae_measurable f (μ.restrict s) ∧ ae_measurable f (μ.restrict t)
@[measurability]
theorem
ae_measurable.smul_measure
{α : Type u_2}
{β : Type u_3}
{R : Type u_6}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[monoid R]
[distrib_mul_action R ennreal]
[is_scalar_tower R ennreal ennreal]
(h : ae_measurable f μ)
(c : R) :
ae_measurable f (c • μ)
theorem
ae_measurable.comp_ae_measurable
{α : Type u_2}
{β : Type u_3}
{δ : Type u_5}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space δ]
{μ : measure_theory.measure α}
{f : α → δ}
{g : δ → β}
(hg : ae_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
ae_measurable (g ∘ f) μ
theorem
ae_measurable.comp_measurable
{α : Type u_2}
{β : Type u_3}
{δ : Type u_5}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space δ]
{μ : measure_theory.measure α}
{f : α → δ}
{g : δ → β}
(hg : ae_measurable g (measure_theory.measure.map f μ))
(hf : measurable f) :
ae_measurable (g ∘ f) μ
theorem
ae_measurable.comp_quasi_measure_preserving
{α : Type u_2}
{β : Type u_3}
{δ : Type u_5}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space δ]
{μ : measure_theory.measure α}
{ν : measure_theory.measure δ}
{f : α → δ}
{g : δ → β}
(hg : ae_measurable g ν)
(hf : measure_theory.measure.quasi_measure_preserving f μ ν) :
ae_measurable (g ∘ f) μ
theorem
ae_measurable.map_map_of_ae_measurable
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{g : β → γ}
{f : α → β}
(hg : ae_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
measure_theory.measure.map g (measure_theory.measure.map f μ) = measure_theory.measure.map (g ∘ f) μ
@[measurability]
theorem
ae_measurable.prod_mk
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{f : α → β}
{g : α → γ}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (x : α), (f x, g x)) μ
theorem
ae_measurable.exists_ae_eq_range_subset
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(H : ae_measurable f μ)
{t : set β}
(ht : ∀ᵐ (x : α) ∂μ, f x ∈ t)
(h₀ : t.nonempty) :
theorem
ae_measurable.exists_measurable_nonneg
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_1}
[preorder β]
[has_zero β]
{mβ : measurable_space β}
{f : α → β}
(hf : ae_measurable f μ)
(f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t) :
theorem
ae_measurable.subtype_mk
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(h : ae_measurable f μ)
{s : set β}
{hfs : ∀ (x : α), f x ∈ s} :
ae_measurable (set.cod_restrict f s hfs) μ
@[protected]
theorem
ae_measurable.null_measurable
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(h : ae_measurable f μ) :
theorem
ae_measurable_const'
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(h : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : α) ∂μ, f x = f y) :
ae_measurable f μ
theorem
ae_measurable_uIoc_iff
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
[linear_order α]
{f : α → β}
{a b : α} :
ae_measurable f (μ.restrict (set.uIoc a b)) ↔ ae_measurable f (μ.restrict (set.Ioc a b)) ∧ ae_measurable f (μ.restrict (set.Ioc b a))
theorem
ae_measurable_iff_measurable
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[μ.is_complete] :
ae_measurable f μ ↔ measurable f
theorem
measurable_embedding.ae_measurable_map_iff
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space γ]
{f : α → β}
{μ : measure_theory.measure α}
{g : β → γ}
(hf : measurable_embedding f) :
ae_measurable g (measure_theory.measure.map f μ) ↔ ae_measurable (g ∘ f) μ
theorem
measurable_embedding.ae_measurable_comp_iff
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space γ]
{f : α → β}
{g : β → γ}
(hg : measurable_embedding g)
{μ : measure_theory.measure α} :
ae_measurable (g ∘ f) μ ↔ ae_measurable f μ
theorem
ae_measurable_restrict_iff_comap_subtype
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{s : set α}
(hs : measurable_set s)
{μ : measure_theory.measure α}
{f : α → β} :
ae_measurable f (μ.restrict s) ↔ ae_measurable (f ∘ coe) (measure_theory.measure.comap coe μ)
@[simp]
theorem
ae_measurable_zero
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
[has_zero β] :
ae_measurable (λ (a : α), 0) μ
@[simp]
theorem
ae_measurable_one
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
[has_one β] :
ae_measurable (λ (a : α), 1) μ
@[simp]
theorem
ae_measurable_smul_measure_iff
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{c : ennreal}
(hc : c ≠ 0) :
ae_measurable f (c • μ) ↔ ae_measurable f μ
theorem
ae_measurable_of_ae_measurable_trim
{β : Type u_3}
[measurable_space β]
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
{f : α → β}
(hf : ae_measurable f (μ.trim hm)) :
ae_measurable f μ
theorem
ae_measurable_restrict_of_measurable_subtype
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(hf : measurable (λ (x : ↥s), f ↑x)) :
ae_measurable f (μ.restrict s)
theorem
ae_measurable_map_equiv_iff
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{m0 : measurable_space α}
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
(e : α ≃ᵐ β)
{f : β → γ} :
ae_measurable f (measure_theory.measure.map ⇑e μ) ↔ ae_measurable (f ∘ ⇑e) μ
theorem
ae_measurable.restrict
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(hfm : ae_measurable f μ)
{s : set α} :
ae_measurable f (μ.restrict s)
theorem
ae_measurable_Ioi_of_forall_Ioc
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_1}
{mβ : measurable_space β}
[linear_order α]
[filter.at_top.is_countably_generated]
{x : α}
{g : α → β}
(g_meas : ∀ (t : α), t > x → ae_measurable g (μ.restrict (set.Ioc x t))) :
ae_measurable g (μ.restrict (set.Ioi x))
theorem
ae_measurable_indicator_iff
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[has_zero β]
{s : set α}
(hs : measurable_set s) :
ae_measurable (s.indicator f) μ ↔ ae_measurable f (μ.restrict s)
@[measurability]
theorem
ae_measurable.indicator
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
[has_zero β]
(hfm : ae_measurable f μ)
{s : set α}
(hs : measurable_set s) :
ae_measurable (s.indicator f) μ
theorem
measure_theory.measure.restrict_map_of_ae_measurable
{α : Type u_2}
{δ : Type u_5}
{m0 : measurable_space α}
[measurable_space δ]
{μ : measure_theory.measure α}
{f : α → δ}
(hf : ae_measurable f μ)
{s : set δ}
(hs : measurable_set s) :
(measure_theory.measure.map f μ).restrict s = measure_theory.measure.map f (μ.restrict (f ⁻¹' s))
theorem
measure_theory.measure.map_mono_of_ae_measurable
{α : Type u_2}
{δ : Type u_5}
{m0 : measurable_space α}
[measurable_space δ]
{μ ν : measure_theory.measure α}
{f : α → δ}
(h : μ ≤ ν)
(hf : ae_measurable f ν) :