mathlib documentation

measure_theory.function.ae_eq_of_integral

From equality of integrals to equality of functions #

This file provides various statements of the general form "if two functions have the same integral on all sets, then they are equal almost everywhere". The different lemmas use various hypotheses on the class of functions, on the target space or on the possible finiteness of the measure.

Main statements #

All results listed below apply to two functions f,g, together with two main hypotheses,

For each of these results, we also provide a lemma about the equality of one function and 0. For example, Lp.ae_eq_zero_of_forall_set_integral_eq_zero.

Generally useful lemmas which are not related to integrals:

theorem measure_theory.ae_eq_zero_of_forall_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [topological_space.second_countable_topology E] {f : α → E} (hf : ∀ (c : E), (λ (x : α), inner c (f x)) =ᵐ[μ] 0) :
f =ᵐ[μ] 0
theorem measure_theory.ae_eq_zero_of_forall_dual {α : Type u_1} {E : Type u_2} (𝕜 : Type u_3) {m : measurable_space α} {μ : measure_theory.measure α} [is_R_or_C 𝕜] [normed_group E] [normed_space 𝕜 E] [topological_space.second_countable_topology E] {f : α → E} (hf : ∀ (c : normed_space.dual 𝕜 E), (λ (x : α), c (f x)) =ᵐ[μ] 0) :
f =ᵐ[μ] 0
theorem measure_theory.ae_const_le_iff_forall_lt_measure_zero {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [linear_order β] [topological_space β] [order_topology β] [topological_space.first_countable_topology β] (f : α → β) (c : β) :
(∀ᵐ (x : α) ∂μ, c f x) ∀ (b : β), b < cμ {x : α | f x b} = 0
theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure_of_measurable {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {f : α → } (hfm : measurable f) (hf : measure_theory.integrable f μ) (hf_zero : ∀ (s : set α), measurable_set s0 (x : α) in s, f x μ) :
0 ≤ᵐ[μ] f

Don't use this lemma. Use ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure.

theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {f : α → } (hf : measure_theory.integrable f μ) (hf_zero : ∀ (s : set α), measurable_set s0 (x : α) in s, f x μ) :
0 ≤ᵐ[μ] f
theorem measure_theory.ae_nonneg_restrict_of_forall_set_integral_nonneg_inter {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → } {t : set α} (hμt : μ t ) (hf : measure_theory.integrable_on f t μ) (hf_zero : ∀ (s : set α), measurable_set s0 (x : α) in s t, f x μ) :
theorem measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_sigma_finite {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} [measure_theory.sigma_finite μ] {f : α → } (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < 0 (x : α) in s, f x μ) :
0 ≤ᵐ[μ] f
theorem measure_theory.ae_fin_strongly_measurable.ae_nonneg_of_forall_set_integral_nonneg {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.ae_fin_strongly_measurable f μ) (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < 0 (x : α) in s, f x μ) :
0 ≤ᵐ[μ] f
theorem measure_theory.integrable.ae_nonneg_of_forall_set_integral_nonneg {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.integrable f μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < 0 (x : α) in s, f x μ) :
0 ≤ᵐ[μ] f
theorem measure_theory.ae_nonneg_restrict_of_forall_set_integral_nonneg {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < 0 (x : α) in s, f x μ) {t : set α} (ht : measurable_set t) (hμt : μ t ) :
theorem measure_theory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero_real {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) {t : set α} (ht : measurable_set t) (hμt : μ t ) :
theorem measure_theory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) {t : set α} (ht : measurable_set t) (hμt : μ t ) :
theorem measure_theory.ae_eq_restrict_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f g : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hfg_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) {t : set α} (ht : measurable_set t) (hμt : μ t ) :
theorem measure_theory.ae_eq_zero_of_forall_set_integral_eq_of_sigma_finite {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [measure_theory.sigma_finite μ] {f : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.ae_eq_of_forall_set_integral_eq_of_sigma_finite {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [measure_theory.sigma_finite μ] {f g : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hfg_eq : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) :
f =ᵐ[μ] g
theorem measure_theory.ae_fin_strongly_measurable.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) (hf : measure_theory.ae_fin_strongly_measurable f μ) :
f =ᵐ[μ] 0
theorem measure_theory.ae_fin_strongly_measurable.ae_eq_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f g : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hfg_eq : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) (hf : measure_theory.ae_fin_strongly_measurable f μ) (hg : measure_theory.ae_fin_strongly_measurable g μ) :
f =ᵐ[μ] g
theorem measure_theory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {p : ℝ≥0∞} (f : (measure_theory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.Lp.ae_eq_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {p : ℝ≥0∞} (f g : (measure_theory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hfg : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) :
theorem measure_theory.ae_eq_zero_of_forall_set_integral_eq_of_fin_strongly_measurable_trim {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] (hm : m m0) {f : α → E} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) (hf : measure_theory.fin_strongly_measurable f (μ.trim hm)) :
f =ᵐ[μ] 0
theorem measure_theory.integrable.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] {f : α → E} (hf : measure_theory.integrable f μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.integrable.ae_eq_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] (f g : α → E) (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) (hfg : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) :
f =ᵐ[μ] g
theorem measure_theory.ae_measurable.ae_eq_of_forall_set_lintegral_eq {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hfi : ∫⁻ (x : α), f x μ ) (hgi : ∫⁻ (x : α), g x μ ) (hfg : ∀ ⦃s : set α⦄, measurable_set sμ s < ∫⁻ (x : α) in s, f x μ = ∫⁻ (x : α) in s, g x μ) :
f =ᵐ[μ] g