From equality of integrals to equality of functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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,
fandgare integrable on all measurable sets with finite measure,- for all measurable sets
swith finite measure,∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ. The conclusion is thenf =ᵐ[μ] g. The main lemmas are: ae_eq_of_forall_set_integral_eq_of_sigma_finite: case of a sigma-finite measure.ae_fin_strongly_measurable.ae_eq_of_forall_set_integral_eq: for functions which areae_fin_strongly_measurable.Lp.ae_eq_of_forall_set_integral_eq: for elements ofLp, for0 < p < ∞.integrable.ae_eq_of_forall_set_integral_eq: for integrable functions.
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.
We also register the corresponding lemma for integrals of ℝ≥0∞-valued functions, in
ae_eq_of_forall_set_lintegral_eq_of_sigma_finite.
Generally useful lemmas which are not related to integrals:
ae_eq_zero_of_forall_inner: if for all constantsc,λ x, inner c (f x) =ᵐ[μ] 0thenf =ᵐ[μ] 0.ae_eq_zero_of_forall_dual: if for all constantscin the dual space,λ x, c (f x) =ᵐ[μ] 0thenf =ᵐ[μ] 0.
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 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[topological_space.second_countable_topology E]
{f : α → E}
(hf : ∀ (c : E), (λ (x : α), has_inner.inner c (f x)) =ᵐ[μ] 0) :
theorem
measure_theory.ae_eq_zero_of_forall_dual_of_is_separable
{α : Type u_1}
{E : Type u_2}
(𝕜 : Type u_3)
{m : measurable_space α}
{μ : measure_theory.measure α}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
{t : set E}
(ht : topological_space.is_separable t)
{f : α → E}
(hf : ∀ (c : normed_space.dual 𝕜 E), (λ (x : α), ⇑c (f x)) =ᵐ[μ] 0)
(h't : ∀ᵐ (x : α) ∂μ, f x ∈ t) :
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_add_comm_group E]
[normed_space 𝕜 E]
[topological_space.second_countable_topology E]
{f : α → E}
(hf : ∀ (c : normed_space.dual 𝕜 E), (λ (x : α), ⇑c (f x)) =ᵐ[μ] 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 : β) :
theorem
measure_theory.ae_le_of_forall_set_lintegral_le_of_sigma_finite
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
{f g : α → ennreal}
(hf : measurable f)
(hg : measurable g)
(h : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) :
theorem
measure_theory.ae_eq_of_forall_set_lintegral_eq_of_sigma_finite
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
{f g : α → ennreal}
(hf : measurable f)
(hg : measurable g)
(h : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) :
theorem
measure_theory.ae_nonneg_of_forall_set_integral_nonneg_of_strongly_measurable
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hfm : measure_theory.strongly_measurable f)
(hf : measure_theory.integrable f μ)
(hf_zero : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) :
Don't use this lemma. Use ae_nonneg_of_forall_set_integral_nonneg.
theorem
measure_theory.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 ∂μ) :
theorem
measure_theory.ae_le_of_forall_set_integral_le
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ)
(hf_le : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ) :
theorem
measure_theory.ae_nonneg_restrict_of_forall_set_integral_nonneg_inter
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
{t : set α}
(hf : measure_theory.integrable_on f t μ)
(hf_zero : ∀ (s : set α), measurable_set s → ⇑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (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 ∂μ) :
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 ∂μ) :
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_add_comm_group E]
[normed_space ℝ 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_add_comm_group E]
[normed_space ℝ 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_add_comm_group E]
[normed_space ℝ 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) :
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_add_comm_group E]
[normed_space ℝ 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 ∂μ) :
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_add_comm_group E]
[normed_space ℝ 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 μ) :
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_add_comm_group E]
[normed_space ℝ 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 μ) :
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_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{p : ennreal}
(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) :
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_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{p : ennreal}
(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_add_comm_group E]
[normed_space ℝ 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)) :
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_add_comm_group E]
[normed_space ℝ 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) :
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_add_comm_group E]
[normed_space ℝ 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 ∂μ) :
theorem
measure_theory.ae_measurable.ae_eq_of_forall_set_lintegral_eq
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ennreal}
(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 ∂μ) :