mathlib documentation

measure_theory.measure.ae_measurable

Almost everywhere measurable functions #

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 α] :
@[measurability]
theorem ae_measurable_of_subsingleton_codomain {α : Type u_2} {β : Type u_3} {m0 : measurable_space α} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} [subsingleton β] :
@[simp, measurability]
theorem ae_measurable_zero_measure {α : Type u_2} {β : Type u_3} {m0 : measurable_space α} [measurable_space β] {f : α → β} :
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' : ν μ) :
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)) :
@[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 μ) :
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)) :
∀ᵐ (x : α) ∂μ, x sf x = ae_measurable.mk f h x
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)) :
@[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 α} :
@[simp]
theorem ae_measurable_add_measure_iff {α : Type u_2} {β : Type u_3} {m0 : measurable_space α} [measurable_space β] {f : α → β} {μ ν : measure_theory.measure α} :
@[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 α} :
@[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) :
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 μ) :
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) :
theorem ae_measurable.comp_measurable' {α : 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 : measurable f) (h : (measure_theory.measure.map f μ).absolutely_continuous ν) :
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 μ) :
@[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) :
∃ (g : α → β), measurable g set.range g t f =ᵐ[μ] g
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) :
∃ (g : α → β), measurable g 0 g f =ᵐ[μ] g
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} :
@[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_interval_oc_iff {α : Type u_2} {β : Type u_3} {m0 : measurable_space α} [measurable_space β] {μ : measure_theory.measure α} [linear_order α] {f : α → β} {a b : α} :
theorem ae_measurable_iff_measurable {α : Type u_2} {β : Type u_3} {m0 : measurable_space α} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} [μ.is_complete] :
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) :
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 α} :
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 : α → β} :
@[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) :
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)) :
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)) :
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 : β → γ} :
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 α} :
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 > xae_measurable g (μ.restrict (set.Ioc x t))) :
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) :
@[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) :
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) :
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 ν) :