Integral with respect to a sum of measures #
In this file we prove that a function f is integrable with respect to a countable sum of measures
Measure.sum μ if and only if f is integrable with respect to each μ i and the sequence
fun i ↦ ∫ x, ‖f x‖ ∂μ i is summable. We then show that under this integrability condition,
∫ x, f x ∂Measure.sum μ = ∑' i, ∫ f x ∂μ i.
We specialize these results to the case where each measure is a Dirac mass,
i.e. μ i = (c i) • .dirac (x i).
Finally we compute integrals over countable and finite spaces or sets.
Main statements #
integrable_sum_measure_iff: A functionfis integrable with respect to a countable sum of measuresMeasure.sum μif and only iffis integrable with respect to eachμ iand the sequencefun i ↦ ∫ x, ‖f x‖ ∂μ iis summable.integrable_sum_dirac_iff: A functionfis integrable with respect to a countable sum of Dirac massesMeasure.sum (fun i ↦ (c i) • Measure.dirac (x i))if and only if the sequencefun i ↦ (c i).toReal * ‖f (x i)‖is summable.hasSum_integral_measure: Iffis integrable with respect toMeasure.sum μ, then the sequencefun i ↦ ∫ x, f x ∂μ iis summable and its sum is∫ x, f x ∂Measure.sum μ.integral_sum_dirac_eq_tsum: If the sequencefun i ↦ (c i).toReal * ‖f (x i)‖is summable, then∑' i, (c i).toReal • f (x i) = ∫ x, f x, ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)).
Tags #
sum of measures, integral, Dirac mass
theorem
MeasureTheory.integrable_sum_measure
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{μ : ι → Measure X}
{f : X → E}
(hf : ∀ (i : ι), Integrable f (μ i))
(h : Summable fun (i : ι) => ∫ (x : X), ‖f x‖ ∂μ i)
:
Integrable f (Measure.sum μ)
theorem
MeasureTheory.Integrable.summable_integral
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{μ : ι → Measure X}
{f : X → E}
(hf : Integrable f (Measure.sum μ))
:
theorem
MeasureTheory.integrable_sum_measure_iff
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{μ : ι → Measure X}
{f : X → E}
:
Integrable f (Measure.sum μ) ↔ (∀ (i : ι), Integrable f (μ i)) ∧ Summable fun (i : ι) => ∫ (x : X), ‖f x‖ ∂μ i
A function f is integrable with respect to a countable sum of measures Measure.sum μ
if and only if f is integrable with respect to each μ i and
the sequence fun i ↦ ∫ x, ‖f x‖ ∂μ i is summable.
theorem
MeasureTheory.integrable_sum_dirac
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[MeasurableSingletonClass X]
{x : ι → X}
{c : ι → ENNReal}
(hc : ∀ (i : ι), c i ≠ ⊤)
(h : Summable fun (i : ι) => (c i).toReal * ‖f (x i)‖)
:
Integrable f (Measure.sum fun (i : ι) => c i • Measure.dirac (x i))
theorem
MeasureTheory.Integrable.summable_of_dirac
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[MeasurableSingletonClass X]
{x : ι → X}
{c : ι → ENNReal}
(hf : Integrable f (Measure.sum fun (i : ι) => c i • Measure.dirac (x i)))
:
theorem
MeasureTheory.integrable_sum_dirac_iff
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[MeasurableSingletonClass X]
{x : ι → X}
{c : ι → ENNReal}
(hc : ∀ (i : ι), c i ≠ ⊤)
:
Integrable f (Measure.sum fun (i : ι) => c i • Measure.dirac (x i)) ↔ Summable fun (i : ι) => (c i).toReal * ‖f (x i)‖
A function f is integrable with respect to a countable sum of
Dirac masses Measure.sum (fun i ↦ (c i) • Measure.dirac (x i)) if and only if
the sequence fun i ↦ (c i).toReal * ‖f (x i)‖ is summable.
theorem
MeasureTheory.hasSum_integral_measure
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{μ : ι → Measure X}
{f : X → E}
[NormedSpace ℝ E]
(hf : Integrable f (Measure.sum μ))
:
If f is integrable with respect to Measure.sum μ, then the sequence
fun i ↦ ∫ x, f x ∂μ i is summable and its sum is ∫ x, f x ∂Measure.sum μ.
theorem
MeasureTheory.integral_sum_measure
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{μ : ι → Measure X}
{f : X → E}
[NormedSpace ℝ E]
(hf : Integrable f (Measure.sum μ))
:
theorem
MeasureTheory.integral_sum_dirac
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[MeasurableSingletonClass X]
{x : ι → X}
{c : ι → ENNReal}
[FiniteDimensional ℝ E]
(hc : ∀ (i : ι), c i ≠ ⊤)
:
theorem
MeasureTheory.hasSum_integral_sum_dirac
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[MeasurableSingletonClass X]
{x : ι → X}
{c : ι → ENNReal}
[CompleteSpace E]
(hc : ∀ (i : ι), c i ≠ ⊤)
(hf : Summable fun (i : ι) => (c i).toReal * ‖f (x i)‖)
:
HasSum (fun (i : ι) => (c i).toReal • f (x i)) (∫ (x : X), f x ∂Measure.sum fun (i : ι) => c i • Measure.dirac (x i))
theorem
MeasureTheory.integral_sum_dirac_eq_tsum
{ι : Type u_1}
{X : Type u_2}
{E : Type u_3}
[Countable ι]
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[MeasurableSingletonClass X]
{x : ι → X}
{c : ι → ENNReal}
[CompleteSpace E]
(hc : ∀ (i : ι), c i ≠ ⊤)
(hf : Summable fun (i : ι) => (c i).toReal * ‖f (x i)‖)
:
If the sequence fun i ↦ (c i).toReal * ‖f (x i)‖ is summable, then
∫ x, f x, ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)) = ∑' i, (c i).toReal • f (x i).
theorem
MeasureTheory.integral_countable
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
{μ : Measure X}
[Countable X]
(hf : Integrable f μ)
:
@[deprecated MeasureTheory.integral_countable (since := "2026-03-09")]
theorem
MeasureTheory.integral_countable'
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
{μ : Measure X}
[Countable X]
(hf : Integrable f μ)
:
Alias of MeasureTheory.integral_countable.
theorem
MeasureTheory.setIntegral_countable
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
{μ : Measure X}
(f : X → E)
{s : Set X}
(hs : s.Countable)
(hf : IntegrableOn f s μ)
:
theorem
MeasureTheory.setIntegral_finset
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
{μ : Measure X}
(s : Finset X)
(hf : IntegrableOn f (↑s) μ)
:
@[deprecated MeasureTheory.setIntegral_finset (since := "2026-03-09")]
theorem
MeasureTheory.integral_finset
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
{μ : Measure X}
(s : Finset X)
(hf : IntegrableOn f (↑s) μ)
:
Alias of MeasureTheory.setIntegral_finset.
theorem
MeasureTheory.integral_fintype
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
{f : X → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
{μ : Measure X}
[Fintype X]
(hf : Integrable f μ)
:
@[simp]
theorem
MeasureTheory.integral_count
{X : Type u_2}
{E : Type u_3}
{mX : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[MeasurableSingletonClass X]
[Fintype X]
(f : X → E)
: