# 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,

• f and g are integrable on all measurable sets with finite measure,
• for all measurable sets s with finite measure, ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ. The conclusion is then f =ᵐ[μ] g. The main lemmas are:
• ae_eq_of_forall_setIntegral_eq_of_sigmaFinite: case of a sigma-finite measure.
• AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq: for functions which are AEFinStronglyMeasurable.
• Lp.ae_eq_of_forall_setIntegral_eq: for elements of Lp, for 0 < p < ∞.
• Integrable.ae_eq_of_forall_setIntegral_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_setIntegral_eq_zero.

We also register the corresponding lemma for integrals of ℝ≥0∞-valued functions, in ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite.

Generally useful lemmas which are not related to integrals:

• ae_eq_zero_of_forall_inner: if for all constants c, fun x => inner c (f x) =ᵐ[μ] 0 then f =ᵐ[μ] 0.
• ae_eq_zero_of_forall_dual: if for all constants c in the dual space, fun x => c (f x) =ᵐ[μ] 0 then f =ᵐ[μ] 0.
theorem MeasureTheory.ae_eq_zero_of_forall_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} {m : } {μ : } [] [] {f : αE} (hf : ∀ (c : E), (fun (x : α) => c, f x⟫_𝕜) =ᵐ[μ] 0) :
f =ᵐ[μ] 0
theorem MeasureTheory.ae_eq_zero_of_forall_dual_of_isSeparable {α : Type u_1} {E : Type u_2} (𝕜 : Type u_3) {m : } {μ : } [] [] {t : Set E} (ht : ) {f : αE} (hf : ∀ (c : ), (fun (x : α) => c (f x)) =ᵐ[μ] 0) (h't : ∀ᵐ (x : α) ∂μ, f x t) :
f =ᵐ[μ] 0
theorem MeasureTheory.ae_eq_zero_of_forall_dual {α : Type u_1} {E : Type u_2} (𝕜 : Type u_3) {m : } {μ : } [] [] {f : αE} (hf : ∀ (c : ), (fun (x : α) => c (f x)) =ᵐ[μ] 0) :
f =ᵐ[μ] 0
theorem MeasureTheory.ae_const_le_iff_forall_lt_measure_zero {α : Type u_1} {m0 : } {μ : } {β : Type u_3} [] [] [] (f : αβ) (c : β) :
(∀ᵐ (x : α) ∂μ, c f x) b < c, μ {x : α | f x b} = 0
theorem MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ) :
f ≤ᵐ[μ] g
@[deprecated MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀]
theorem MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ) :
f ≤ᵐ[μ] g

Alias of MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀.

theorem MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ) :
f ≤ᵐ[μ] g
@[deprecated MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite]
theorem MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ ∫⁻ (x : α) in s, g xμ) :
f ≤ᵐ[μ] g

Alias of MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite.

theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀]
theorem MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ) :
f =ᵐ[μ] g

Alias of MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀.

theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite]
theorem MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (h : ∀ (s : Set α), μ s < ∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ) :
f =ᵐ[μ] g

Alias of MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite.

theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f
@[deprecated MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg]
theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f

Alias of MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg.

@[deprecated MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg]
theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_stronglyMeasurable {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f

Alias of MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg.

@[deprecated MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg]
theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f

Alias of MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg.

theorem MeasureTheory.ae_le_of_forall_setIntegral_le {α : Type u_1} {m0 : } {μ : } {f : α} {g : α} (hf : ) (hg : ) (hf_le : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ ∫ (x : α) in s, g xμ) :
f ≤ᵐ[μ] g
@[deprecated MeasureTheory.ae_le_of_forall_setIntegral_le]
theorem MeasureTheory.ae_le_of_forall_set_integral_le {α : Type u_1} {m0 : } {μ : } {f : α} {g : α} (hf : ) (hg : ) (hf_le : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ ∫ (x : α) in s, g xμ) :
f ≤ᵐ[μ] g

Alias of MeasureTheory.ae_le_of_forall_setIntegral_le.

theorem MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter {α : Type u_1} {m0 : } {μ : } {f : α} {t : Set α} (hf : ) (hf_zero : ∀ (s : Set α), μ (s t) < 0 ∫ (x : α) in s t, f xμ) :
0 ≤ᵐ[μ.restrict t] f
@[deprecated MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter]
theorem MeasureTheory.ae_nonneg_restrict_of_forall_set_integral_nonneg_inter {α : Type u_1} {m0 : } {μ : } {f : α} {t : Set α} (hf : ) (hf_zero : ∀ (s : Set α), μ (s t) < 0 ∫ (x : α) in s t, f xμ) :
0 ≤ᵐ[μ.restrict t] f

Alias of MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter.

theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite {α : Type u_1} {m0 : } {μ : } {f : α} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f
@[deprecated MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite]
theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_sigmaFinite {α : Type u_1} {m0 : } {μ : } {f : α} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f

Alias of MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite.

theorem MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f
@[deprecated MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg]
theorem MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_set_integral_nonneg {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) :
0 ≤ᵐ[μ] f

Alias of MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg.

theorem MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg {α : Type u_1} {m0 : } {μ : } {f : α} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) {t : Set α} (ht : ) (hμt : μ t ) :
0 ≤ᵐ[μ.restrict t] f
@[deprecated MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg]
theorem MeasureTheory.ae_nonneg_restrict_of_forall_set_integral_nonneg {α : Type u_1} {m0 : } {μ : } {f : α} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < 0 ∫ (x : α) in s, f xμ) {t : Set α} (ht : ) (hμt : μ t ) :
0 ≤ᵐ[μ.restrict t] f

Alias of MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg.

theorem MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real {α : Type u_1} {m0 : } {μ : } {f : α} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) {t : Set α} (ht : ) (hμt : μ t ) :
f =ᵐ[μ.restrict t] 0
@[deprecated MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real]
theorem MeasureTheory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero_real {α : Type u_1} {m0 : } {μ : } {f : α} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) {t : Set α} (ht : ) (hμt : μ t ) :
f =ᵐ[μ.restrict t] 0

Alias of MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real.

theorem MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) {t : Set α} (ht : ) (hμt : μ t ) :
f =ᵐ[μ.restrict t] 0
@[deprecated MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero]
theorem MeasureTheory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) {t : Set α} (ht : ) (hμt : μ t ) :
f =ᵐ[μ.restrict t] 0

Alias of MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero.

theorem MeasureTheory.ae_eq_restrict_of_forall_setIntegral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} {g : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) {t : Set α} (ht : ) (hμt : μ t ) :
f =ᵐ[μ.restrict t] g
@[deprecated MeasureTheory.ae_eq_restrict_of_forall_setIntegral_eq]
theorem MeasureTheory.ae_eq_restrict_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} {g : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) {t : Set α} (ht : ) (hμt : μ t ) :
f =ᵐ[μ.restrict t] g

Alias of MeasureTheory.ae_eq_restrict_of_forall_setIntegral_eq.

theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite]
theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_eq_of_sigmaFinite {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0

Alias of MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite.

theorem MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} {g : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_eq : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite]
theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} {g : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_eq : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) :
f =ᵐ[μ] g

Alias of MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite.

theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) (hf : ) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero]
theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) (hf : ) :
f =ᵐ[μ] 0

Alias of MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero.

theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} {g : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_eq : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) (hf : ) (hg : ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq]
theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} {g : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_eq : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) (hf : ) (hg : ) :
f =ᵐ[μ] g

Alias of MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq.

theorem MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {p : ENNReal} (f : (MeasureTheory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (↑f) s μ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero]
theorem MeasureTheory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {p : ENNReal} (f : (MeasureTheory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (↑f) s μ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0

Alias of MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero.

theorem MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {p : ENNReal} (f : (MeasureTheory.Lp E p μ)) (g : (MeasureTheory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (↑f) s μ) (hg_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (↑g) s μ) (hfg : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq]
theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {p : ENNReal} (f : (MeasureTheory.Lp E p μ)) (g : (MeasureTheory.Lp E p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (↑f) s μ) (hg_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (↑g) s μ) (hfg : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) :
f =ᵐ[μ] g

Alias of MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq.

theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim {α : Type u_1} {E : Type u_2} {m : } {m0 : } {μ : } [] [] (hm : m m0) {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) (hf : MeasureTheory.FinStronglyMeasurable f (μ.trim hm)) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim]
theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_eq_of_finStronglyMeasurable_trim {α : Type u_1} {E : Type u_2} {m : } {m0 : } {μ : } [] [] (hm : m m0) {f : αE} (hf_int_finite : ∀ (s : Set α), μ s < ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) (hf : MeasureTheory.FinStronglyMeasurable f (μ.trim hm)) :
f =ᵐ[μ] 0

Alias of MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim.

theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf : ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero]
theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : αE} (hf : ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0

Alias of MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero.

theorem MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] (f : αE) (g : αE) (hf : ) (hg : ) (hfg : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq]
theorem MeasureTheory.Integrable.ae_eq_of_forall_set_integral_eq {α : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] (f : αE) (g : αE) (hf : ) (hg : ) (hfg : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) :
f =ᵐ[μ] g

Alias of MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq.

theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero {E : Type u_2} [] [] {β : Type u_3} [] [] [] {μ : } {f : βE} (hf : ) (h'f : ∀ (s : Set β), ∫ (x : β) in s, f xμ = 0) :
f =ᵐ[μ] 0

If an integrable function has zero integral on all closed sets, then it is zero almost everwhere.

@[deprecated MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero]
theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_isClosed_eq_zero {E : Type u_2} [] [] {β : Type u_3} [] [] [] {μ : } {f : βE} (hf : ) (h'f : ∀ (s : Set β), ∫ (x : β) in s, f xμ = 0) :
f =ᵐ[μ] 0

Alias of MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero.

If an integrable function has zero integral on all closed sets, then it is zero almost everwhere.

theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero {E : Type u_2} [] [] {β : Type u_3} [] [] [] [] {μ : } {f : βE} (hf : ) (h'f : ∀ (s : Set β), ∫ (x : β) in s, f xμ = 0) :
f =ᵐ[μ] 0

If an integrable function has zero integral on all compact sets in a sigma-compact space, then it is zero almost everwhere.

theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' {E : Type u_2} [] [] {β : Type u_3} [] [] [] [] {μ : } {f : βE} (hf : ) (h'f : ∀ (s : Set β), ∫ (x : β) in s, f xμ = 0) :
f =ᵐ[μ] 0

If a locally integrable function has zero integral on all compact sets in a sigma-compact space, then it is zero almost everwhere.

theorem MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (hfi : ∫⁻ (x : α), f xμ ) (hgi : ∫⁻ (x : α), g xμ ) (hfg : ∀ ⦃s : Set α⦄, μ s < ∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq]
theorem MeasureTheory.AEMeasurable.ae_eq_of_forall_set_lintegral_eq {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (hfi : ∫⁻ (x : α), f xμ ) (hgi : ∫⁻ (x : α), g xμ ) (hfg : ∀ ⦃s : Set α⦄, μ s < ∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in s, g xμ) :
f =ᵐ[μ] g

Alias of MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq.

theorem MeasureTheory.withDensity_eq_iff_of_sigmaFinite {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) :
μ.withDensity f = μ.withDensity g f =ᵐ[μ] g
theorem MeasureTheory.withDensity_eq_iff {α : Type u_1} {m : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) (hfi : ∫⁻ (x : α), f xμ ) :
μ.withDensity f = μ.withDensity g f =ᵐ[μ] g