Extended Real Integral #
This file defines integration for functions taking values in EReal (the extended reals).
Main definitions #
eintegral: The integral of anEReal-valued function, defined as the difference between the lower Lebesgue integrals of the positive and negative parts.EIntegrable: A condition ensuring the integral is well-defined (avoiding⊤ - ⊤).- instances for positive and negative parts of an
EReal-valued function.
Main statements #
eintegral_add: The integral of a sum is the sum of integrals (under suitable integrability conditions to avoid indeterminate forms).eintegral_sub: The integral of a difference is the difference of integrals (under suitable integrability conditions).eintegral_prod: Fubini's theorem for extended real-valued functions on product measures, allowing interchange of integration order.limsup_eintegral_le: A Fatou-type lemma for the extended integral, relating the limsup of integrals to the integral of the limsup.eintegral_liminf_le: A Fatou-type lemma for the extended integral, relating the liminf of integrals to the integral of the liminf.
Notation #
∫ᵉ x, f x ∂μ: The extended integral offwith respect to measureμ.f⁺andf⁻: Positive and negative parts of a function.
noncomputable def
MeasureTheory.eintegral
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
(f : α → EReal)
:
The integral of an EReal-valued function with respect to a measure μ, defined as the
difference of two lower Lebesgue integrals.
Equations
Instances For
The integral of an EReal-valued function with respect to a measure μ, defined as the
difference of two lower Lebesgue integrals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integral of an EReal-valued function with respect to a measure μ, defined as the
difference of two lower Lebesgue integrals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integral of an EReal-valued function with respect to a measure μ, defined as the
difference of two lower Lebesgue integrals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integral of an EReal-valued function with respect to a measure μ, defined as the
difference of two lower Lebesgue integrals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.EIntegrable
{α : Type u_1}
{mα : MeasurableSpace α}
(f : α → EReal)
(μ : Measure α := by volume_tac)
:
Condition for a function to have a well-defined extended integral,
avoiding the ⊤ - ⊤ bad case in the definition.
Equations
Instances For
theorem
MeasureTheory.eintegrable_congr
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(h_ae : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.eintegrable_of_nonneg
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : ∀ (x : α), 0 ≤ f x)
:
EIntegrable f μ
theorem
MeasureTheory.eintegrable_of_nonpos
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : ∀ (x : α), f x ≤ 0)
:
EIntegrable f μ
theorem
MeasureTheory.eintegrable_const
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{c : EReal}
:
EIntegrable (fun (x : α) => c) μ
theorem
MeasureTheory.EIntegrable.neg
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : EIntegrable f μ)
:
EIntegrable (fun (x : α) => -f x) μ
theorem
MeasureTheory.EIntegrable.const_mul
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{c : EReal}
{f : α → EReal}
(hf : EIntegrable f μ)
(hc_bot : c ≠ ⊥)
(hc_top : c ≠ ⊤)
:
EIntegrable (fun (x : α) => c * f x) μ
theorem
MeasureTheory.EIntegrable.add_const
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{c : EReal}
{f : α → EReal}
(hf : EIntegrable f μ)
(hc_bot : c ≠ ⊥)
(hc_top : c ≠ ⊤)
:
EIntegrable (fun (x : α) => f x + c) μ
theorem
MeasureTheory.EIntegrable.sub_const
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{c : EReal}
{f : α → EReal}
(hf : EIntegrable f μ)
(hc_bot : c ≠ ⊥)
(hc_top : c ≠ ⊤)
:
EIntegrable (fun (x : α) => f x - c) μ
theorem
MeasureTheory.EIntegrable.smul_measure
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{X : α → EReal}
(hX : EIntegrable X μ)
{c : ENNReal}
(hc : c ≠ ⊤)
:
EIntegrable X (c • μ)
theorem
MeasureTheory.eintegrable_map
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → EReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g (Measure.map f μ))
:
theorem
MeasureTheory.eintegrable_of_le
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
{b : EReal}
(hf : ∀ (x : α), f x ≤ b)
(hb : b ≠ ⊤)
(P : Measure α)
[IsFiniteMeasure P]
:
EIntegrable f P
theorem
MeasureTheory.Measurable.posPartFun
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
(hf : Measurable f)
:
Measurable fun (x : α) => f⁺ x
theorem
MeasureTheory.Measurable.negPartFun
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → EReal}
(hf : Measurable f)
:
Measurable fun (x : α) => f⁻ x
theorem
MeasureTheory.AEMeasurable.posPartFun
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => f⁺ x) μ
theorem
MeasureTheory.AEMeasurable.negPartFun
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => f⁻ x) μ
@[simp]
theorem
MeasureTheory.eintegral_of_not_eintegrable
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : ¬EIntegrable f μ)
:
theorem
MeasureTheory.eintegrable_of_eintegral_ne_bot
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf : ∫ᵉ (x : α), f x ∂μ ≠ ⊥)
:
EIntegrable f μ
@[simp]
@[simp]
theorem
MeasureTheory.eintegral_zero_measure
{α : Type u_1}
{mα : MeasurableSpace α}
(f : α → EReal)
:
theorem
MeasureTheory.eintegral_nonneg'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf_meas : AEMeasurable f μ)
(hf : ∀ᵐ (x : α) ∂μ, 0 ≤ f x)
:
theorem
MeasureTheory.eintegral_nonpos'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf_meas : AEMeasurable f μ)
(hf : ∀ᵐ (x : α) ∂μ, f x ≤ 0)
:
theorem
MeasureTheory.eintegral_strict_mono_ae
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hμ : μ ≠ 0)
(hg : AEMeasurable g μ)
(hf : AEMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, f x < g x)
(hfi : ∫ᵉ (x : α), f x ∂μ < ⊤)
(hgi : ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
The extended integral is strictly monotone with respect to almost-everywhere strict inequality.
theorem
MeasureTheory.eintegral_strict_mono
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hμ : μ ≠ 0)
(hg : AEMeasurable g μ)
(hf : AEMeasurable f μ)
(hfg : ∀ (x : α), f x < g x)
(hfi : ∫ᵉ (x : α), f x ∂μ < ⊤)
(hgi : ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
theorem
MeasureTheory.eintegral_eq_posPartFun_sub_negPartFun
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
(f : α → EReal)
:
The extended integral decomposes as the difference between the integrals of the positive and negative parts of the function.
theorem
MeasureTheory.eintegral_eq_integral
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
:
For Integrable real-valued functions, the extended integral coincides with the
standard Bochner integral.
theorem
MeasureTheory.integrable_toReal
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf_meas : AEMeasurable f μ)
(h_int_bot : ∫ᵉ (x : α), f x ∂μ ≠ ⊥)
(h_int_top : ∫ᵉ (x : α), f x ∂μ ≠ ⊤)
:
Integrable (fun (x : α) => (f x).toReal) μ
theorem
MeasureTheory.eintegral_eq_integral_toReal
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : α → EReal}
(hf_meas : AEMeasurable f μ)
(h_int_bot : ∫ᵉ (x : α), f x ∂μ ≠ ⊥)
(h_int_top : ∫ᵉ (x : α), f x ∂μ ≠ ⊤)
:
If the extended integral is finite, then it equals the integral of the real part.
theorem
MeasureTheory.eintegral_add_of_nonneg_of_measurable'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf_meas : Measurable f)
(hg_meas : Measurable g)
(hf : ∀ᵐ (x : α) ∂μ, 0 ≤ f x)
(hg : ∀ᵐ (x : α) ∂μ, 0 ≤ g x)
:
theorem
MeasureTheory.eintegral_add_of_nonneg'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf_meas : AEMeasurable f μ)
(hg_meas : AEMeasurable g μ)
(hf : ∀ᵐ (x : α) ∂μ, 0 ≤ f x)
(hg : ∀ᵐ (x : α) ∂μ, 0 ≤ g x)
:
theorem
MeasureTheory.eintegral_sub_of_nonneg
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf : ∀ (x : α), 0 ≤ f x)
(hg : ∀ (x : α), 0 ≤ g x)
(hf_meas : AEMeasurable f μ)
(hg_meas : AEMeasurable g μ)
(hfg : ∫ᵉ (x : α), min (f x) (g x) ∂μ ≠ ⊤)
:
theorem
MeasureTheory.eintegral_add
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
(hf_int : EIntegrable f μ)
(hg_int : EIntegrable g μ)
(h_ne_bot_1 : ∫ᵉ (x : α), f x ∂μ ≠ ⊥ ∨ ∫ᵉ (x : α), g x ∂μ ≠ ⊤)
(h_ne_bot_2 : ∫ᵉ (x : α), f x ∂μ ≠ ⊤ ∨ ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
The integral of a sum is the sum of integrals (requires compatibility conditions to
avoid ⊤ - ⊤).
theorem
MeasureTheory.eintegral_add'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
(hg_ne_top : ∫ᵉ (x : α), g x ∂μ ≠ ⊤)
(hg_ne_bot : ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
theorem
MeasureTheory.eintegral_sub
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf : EIntegrable f μ)
(hf_meas : AEMeasurable f μ)
(hg : EIntegrable g μ)
(hg_meas : AEMeasurable g μ)
(h_ne_top : ∫ᵉ (x : α), f x ∂μ ≠ ⊤ ∨ ∫ᵉ (x : α), g x ∂μ ≠ ⊤)
(h_ne_bot : ∫ᵉ (x : α), f x ∂μ ≠ ⊥ ∨ ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
The integral of a difference is the difference of integrals (requires compatibility
conditions to avoid ⊤ - ⊤).
theorem
MeasureTheory.eintegral_sub'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf_meas : AEMeasurable f μ)
(hg_meas : AEMeasurable g μ)
(hg_ne_top : ∫ᵉ (x : α), g x ∂μ ≠ ⊤)
(hg_ne_bot : ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
theorem
MeasureTheory.eintegral_sub''
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf_meas : AEMeasurable f μ)
(hg_meas : AEMeasurable g μ)
(hf_ne_top : ∫ᵉ (x : α), f x ∂μ ≠ ⊤)
(hf_ne_bot : ∫ᵉ (x : α), f x ∂μ ≠ ⊥)
(hg_int : EIntegrable g μ)
:
theorem
MeasureTheory.eintegrable_add_of_ne_bot
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f g : α → EReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
(hf_int : ∫ᵉ (x : α), f x ∂μ ≠ ⊥)
(hg_int : ∫ᵉ (x : α), g x ∂μ ≠ ⊥)
:
EIntegrable (fun (x : α) => f x + g x) μ
theorem
MeasureTheory.eintegral_prod_of_nonneg
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{ν : Measure β}
[SFinite ν]
(f : α × β → EReal)
(hf : AEMeasurable f (μ.prod ν))
(hf_nonneg : ∀ (x : α × β), 0 ≤ f x)
:
theorem
MeasureTheory.eintegral_map
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{f : β → EReal}
{g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
theorem
MeasureTheory.eintegral_map'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{f : β → EReal}
{g : α → β}
(hf : AEMeasurable f (Measure.map g μ))
(hg : AEMeasurable g μ)
:
theorem
MeasureTheory.eintegral_bind_of_nonneg
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m : α → Measure β}
{f : β → EReal}
(hf_nonneg : ∀ (x : β), 0 ≤ f x)
(hμ : AEMeasurable m μ)
(hf : AEMeasurable f (μ.bind m))
:
theorem
MeasureTheory.eintegral_comp_measure
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{f : β → EReal}
(hf : Measurable f)
(hf_int : EIntegrable f (μ.bind ⇑κ))
:
theorem
MeasureTheory.eintegral_comp_measure_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{f : β → EReal}
(hf : Measurable f)
:
@[simp]
theorem
MeasureTheory.eintegral_dirac
{α : Type u_2}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{x₀ : α}
{f : α → EReal}
:
theorem
MeasureTheory.eintegral_coe_ennreal_sub
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{u v : α → ENNReal}
(hu : AEMeasurable u μ)
(hv : AEMeasurable v μ)
(h : ∫⁻ (x : α), u x ∂μ ≠ ⊤ ∨ ∫⁻ (x : α), v x ∂μ ≠ ⊤)
:
The extended integral of the difference of two ENNReal-valued functions (coerced to EReal) is the difference of their Lebesgue integrals, provided at least one of the integrals is finite.
theorem
MeasureTheory.eintegral_prod
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
{ν : Measure β}
[SFinite ν]
(f : α × β → EReal)
(hf : AEMeasurable f (μ.prod ν))
(hf_int : EIntegrable f (μ.prod ν))
:
Fubini's theorem for extended reals: the integral over the product equals the iterated integral.
theorem
MeasureTheory.eintegral_prod_symm
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[SFinite μ]
{ν : Measure β}
[SFinite ν]
(f : α × β → EReal)
(hf : AEMeasurable f (μ.prod ν))
(hf_int : EIntegrable f (μ.prod ν))
:
theorem
MeasureTheory.limsup_eintegral_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : ℕ → α → EReal}
(hf : ∀ (n : ℕ), Measurable (f n))
{g : α → ENNReal}
(h_bound : ∀ (n : ℕ), EReal.toENNReal ∘ f n ≤ᶠ[ae μ] g)
(h_fin : ∫⁻ (x : α), g x ∂μ ≠ ⊤)
(fin_limsup :
Filter.limsup (fun (n : ℕ) => ↑(∫⁻ (x : α), (f n x).toENNReal ∂μ)) Filter.atTop ≠ ⊤ ∨ Filter.limsup (fun (n : ℕ) => -↑(∫⁻ (x : α), (-f n x).toENNReal ∂μ)) Filter.atTop ≠ ⊥)
:
Filter.limsup (fun (n : ℕ) => ∫ᵉ (x : α), f n x ∂μ) Filter.atTop ≤ ∫ᵉ (x : α), Filter.limsup (fun (n : ℕ) => f n x) Filter.atTop ∂μ
Fatou's lemma on limsup for the extended integral.
theorem
MeasureTheory.eintegral_liminf_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{f : ℕ → α → EReal}
(hf : ∀ (n : ℕ), Measurable (f n))
{g : α → ENNReal}
(h_bound : ∀ (n : ℕ), EReal.toENNReal ∘ (-f n) ≤ᶠ[ae μ] g)
(h_fin : ∫⁻ (x : α), g x ∂μ ≠ ⊤)
:
∫ᵉ (x : α), Filter.liminf (fun (n : ℕ) => f n x) Filter.atTop ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫ᵉ (x : α), f n x ∂μ) Filter.atTop
Fatou's lemma on liminf for the extended integral.