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

This file is about Lebesgue integrals. See the file `AEEqOfIntegral` for Bochner integrals.

## Main statements #

The results listed below apply to two functions `f, g`, under the hypothesis that 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_setLIntegral_eq_of_sigmaFinite`: case of a sigma-finite measure.
- `AEMeasurable.ae_eq_of_forall_setLIntegral_eq`: for functions which are `AEMeasurable` and have finite integral.

source
theorem MeasureTheory.ae_const_le_iff_forall_lt_measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [FirstCountableTopology β] (f : α → β) (c : β) :
(∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x : α | f x ≤ b} = 0
source
theorem MeasureTheory.ae_le_const_iff_forall_gt_measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {β : Type u_2} [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [FirstCountableTopology β] {μ : Measure α} (f : α → β) (c : β) :
(∀ᵐ (x : α) ∂μ, f x ≤ c) ↔ ∀ (b : β), c < b → μ {x : α | b ≤ f x} = 0
source
theorem MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f g : α → ENNReal} (hf : AEMeasurable f μ) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) :
f ≤ᶠ[ae μ] g
source
theorem MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f g : α → ENNReal} (hf : Measurable f) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) :
f ≤ᶠ[ae μ] g
source
theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) :
f =ᶠ[ae μ] g
source
theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) :
f =ᶠ[ae μ] g
source
theorem MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤) (hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ) :
f =ᶠ[ae μ] g
source
theorem MeasureTheory.lintegral_eq_lintegral_of_isPiSystem {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set (Set α)} {f g : α → ENNReal} (h_eq : m0 = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ) (h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ) (hf_int : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (t : Set α) :
MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
source
theorem MeasureTheory.lintegral_eq_lintegral_of_isPiSystem_of_univ_mem {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set (Set α)} {f g : α → ENNReal} (h_eq : m0 = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (h_univ : Set.univ ∈ s) (basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ) (hf_int : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {t : Set α} (ht : MeasurableSet t) :
∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
source
theorem MeasureTheory.ae_eq_of_setLIntegral_prod_eq {α : Type u_1} {m0 : MeasurableSpace α} {β : Type u_2} {mβ : MeasurableSpace β} {μ : Measure (α × β)} {f g : α × β → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ⊤) (h : ∀ ⦃s : Set α⦄, MeasurableSet s → ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ) :
f =ᶠ[ae μ] g

If two a.e.-measurable functions `α × β → ℝ≥0∞` with finite integrals have the same integral on every rectangle, then they are almost everywhere equal.

source
theorem MeasureTheory.withDensity_eq_iff_of_sigmaFinite {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
μ.withDensity f = μ.withDensity g ↔ f =ᶠ[ae μ] g
source
theorem MeasureTheory.withDensity_eq_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
μ.withDensity f = μ.withDensity g ↔ f =ᶠ[ae μ] g