Documentation

Mathlib.MeasureTheory.Measure.Sum

Sums of measures #

Given μ : ι → Measure α, we define Measure.sum μ as the measure which to a measurable set s associates ∑' i, μ i s.

Tags #

measure, sum

source
noncomputable def MeasureTheory.Measure.sum {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (μ : ι → Measure α) :
Measure α

Sum of an indexed family of measures.

Equations
Instances For
    source
    theorem MeasureTheory.Measure.le_sum_apply {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (μ : ι → Measure α) (s : Set α) :
    ∑' (i : ι), (μ i) s ≤ (sum μ) s
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_apply {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {s : Set α} (μ : ι → Measure α) (hs : MeasurableSet s) :
    (sum μ) s = ∑' (i : ι), (μ i) s
    source
    theorem MeasureTheory.Measure.sum_apply₀ {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {s : Set α} (μ : ι → Measure α) (hs : NullMeasurableSet s (sum μ)) :
    (sum μ) s = ∑' (i : ι), (μ i) s

    For the next theorem, the countability assumption is necessary. For a counterexample, consider an uncountable space, with a distinguished point x₀, and the sigma-algebra made of countable sets not containing x₀, and their complements. All points but x₀ are measurable. Consider the sum of the Dirac masses at points different from x₀, and s = {x₀}. For any Dirac mass δ_x, we have δ_x (x₀) = 0, so ∑' x, δ_x (x₀) = 0. On the other hand, the measure sum δ_x gives mass one to each point different from x₀, so it gives infinite mass to any measurable set containing x₀ (as such a set is uncountable), and by outer regularity one gets sum δ_x {x₀} = ∞.

    source
    theorem MeasureTheory.Measure.sum_apply_of_countable {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} [Countable ι] (μ : ι → Measure α) (s : Set α) :
    (sum μ) s = ∑' (i : ι), (μ i) s
    source
    theorem MeasureTheory.Measure.le_sum {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (μ : ι → Measure α) (i : ι) :
    μ i ≤ sum μ
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_apply_eq_zero {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {s : Set α} {μ : ι → Measure α} [Countable ι] :
    (sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
    source
    theorem MeasureTheory.Measure.sum_apply_eq_zero' {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {s : Set α} {μ : ι → Measure α} (hs : MeasurableSet s) :
    (sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_eq_zero {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {μ : ι → Measure α} :
    sum μ = 0 ↔ ∀ (i : ι), μ i = 0
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_zero {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} :
    (sum fun (x : ι) => 0) = 0
    source
    theorem MeasureTheory.Measure.sum_sum {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {mα : MeasurableSpace α} (μ : ι → ι' → Measure α) :
    (sum fun (n : ι) => sum (μ n)) = sum fun (p : ι × ι') => μ p.1 p.2
    source
    theorem MeasureTheory.Measure.sum_comm {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {mα : MeasurableSpace α} (μ : ι → ι' → Measure α) :
    (sum fun (n : ι) => sum (μ n)) = sum fun (m : ι') => sum fun (n : ι) => μ n m
    source
    theorem MeasureTheory.Measure.ae_sum_iff {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {μ : ι → Measure α} [Countable ι] {p : α → Prop} :
    (∀ᵐ (x : α) ∂sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
    source
    theorem MeasureTheory.Measure.ae_sum_iff' {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {μ : ι → Measure α} {p : α → Prop} (h : MeasurableSet {x : α | p x}) :
    (∀ᵐ (x : α) ∂sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_fintype {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} [Fintype ι] (μ : ι → Measure α) :
    sum μ = ∑ i : ι, μ i
    source
    theorem MeasureTheory.Measure.sum_coe_finset {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (s : Finset ι) (μ : ι → Measure α) :
    (sum fun (i : ↥s) => μ ↑i) = ∑ i ∈ s, μ i
    source
    @[simp]
    theorem MeasureTheory.Measure.ae_sum_eq {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} [Countable ι] (μ : ι → Measure α) :
    ae (sum μ) = ⨆ (i : ι), ae (μ i)
    source
    theorem MeasureTheory.Measure.sum_bool {α : Type u_1} {mα : MeasurableSpace α} (μ : Bool → Measure α) :
    sum μ = μ true + μ false
    source
    theorem MeasureTheory.Measure.sum_cond {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) :
    (sum fun (b : Bool) => bif b then μ else ν) = μ + ν
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_of_isEmpty {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} [IsEmpty ι] (μ : ι → Measure α) :
    sum μ = 0
    source
    theorem MeasureTheory.Measure.sum_add_sum_compl {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (s : Set ι) (μ : ι → Measure α) :
    ((sum fun (i : ↑s) => μ ↑i) + sum fun (i : ↑sᶜ) => μ ↑i) = sum μ
    source
    theorem MeasureTheory.Measure.sum_congr {α : Type u_1} {mα : MeasurableSpace α} {μ ν : ℕ → Measure α} (h : ∀ (n : ℕ), μ n = ν n) :
    sum μ = sum ν
    source
    theorem MeasureTheory.Measure.sum_add_sum {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (μ ν : ι → Measure α) :
    sum μ + sum ν = sum fun (n : ι) => μ n + ν n
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_comp_equiv {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {mα : MeasurableSpace α} (e : ι' ≃ ι) (μ : ι → Measure α) :
    sum (μ ∘ ⇑e) = sum μ
    source
    @[simp]
    theorem MeasureTheory.Measure.sum_extend_zero {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {mα : MeasurableSpace α} {f : ι → ι'} (hf : Function.Injective f) (μ : ι → Measure α) :
    sum (Function.extend f μ 0) = sum μ