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 areAEMeasurableand have finite integral.
theorem
MeasureTheory.ae_const_le_iff_forall_lt_measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
[LinearOrder β]
[TopologicalSpace β]
[OrderTopology β]
[FirstCountableTopology β]
(f : α → β)
(c : β)
:
theorem
MeasureTheory.ae_le_const_iff_forall_gt_measure_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{β : Type u_2}
[LinearOrder β]
[TopologicalSpace β]
[OrderTopology β]
[FirstCountableTopology β]
{μ : MeasureTheory.Measure α}
(f : α → β)
(c : β)
:
theorem
MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ)
:
@[deprecated MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ (since := "2024-06-29")]
theorem
MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ)
:
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal}
(hf : Measurable f)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ)
:
@[deprecated MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite (since := "2024-06-29")]
theorem
MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal}
(hf : Measurable f)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ)
:
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.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 ∂μ)
:
@[deprecated MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ (since := "2024-06-29")]
theorem
MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.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 ∂μ)
:
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.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 ∂μ)
:
@[deprecated MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (since := "2024-06-29")]
theorem
MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.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 ∂μ)
:
Alias of MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite.
theorem
MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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 ∂μ)
:
@[deprecated MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq (since := "2024-06-29")]
theorem
MeasureTheory.AEMeasurable.ae_eq_of_forall_set_lintegral_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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 ∂μ)
:
Alias of MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq.
theorem
MeasureTheory.withDensity_eq_iff_of_sigmaFinite
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
theorem
MeasureTheory.withDensity_eq_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
: