Documentation

Linglib.Core.MeasureTheory.Measure.Dirac

Dirac measures and their finite sums #

A Dirac measure is a zero-one measure, and a probability measure almost surely equal to a point is the Dirac measure at it. On a finite type with measurable singletons, ∑ b, w b • dirac b gives a set the total weight of its points; Measure.ofWeights w names it. With nonnegative real weights its real values are sums of those weights, and it is a probability measure when they sum to one. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/Dirac.lean.

source
instance MeasureTheory.Measure.instIsZeroOneMeasureDirac_linglib {α : Type u_1} [MeasurableSpace α] (a : α) :
IsZeroOneMeasure (dirac a)
source
theorem MeasureTheory.Measure.eq_dirac_of_ae_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {μ : Measure α} [IsProbabilityMeasure μ] {a : α} (h : ∀ᵐ (x : α) ∂μ, x = a) :
μ = dirac a

A probability measure almost surely equal to a point is the Dirac measure at it.

source
theorem MeasureTheory.Measure.sum_smul_dirac_apply {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] (w : β → ENNReal) (s : Set β) :
(∑ b : β, w b • dirac b) s = ∑ b : β, s.indicator w b

A finite sum of scaled Dirac measures gives a set the total weight of its points.

source
theorem MeasureTheory.Measure.sum_smul_dirac_apply_singleton {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] (w : β → ENNReal) (b : β) :
(∑ b' : β, w b' • dirac b') {b} = w b

A finite sum of scaled Dirac measures evaluates at a singleton to its weight.

source
theorem MeasureTheory.Measure.sum_ofReal_smul_dirac_real_apply {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] {w : β → ℝ} (hw : ∀ (b : β), 0 ≤ w b) (s : Set β) :
(∑ b : β, ENNReal.ofReal (w b) • dirac b).real s = ∑ b : β, s.indicator w b

With nonnegative real weights, a finite sum of Dirac measures gives a set, on reals, the total weight of its points.

source
theorem MeasureTheory.Measure.isProbabilityMeasure_sum_ofReal_smul_dirac {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] {w : β → ℝ} (hw : ∀ (b : β), 0 ≤ w b) (h : ∑ b : β, w b = 1) :
IsProbabilityMeasure (∑ b : β, ENNReal.ofReal (w b) • dirac b)

Nonnegative real weights summing to one give a probability measure.

source
noncomputable def MeasureTheory.Measure.ofWeights {β : Type u_1} [MeasurableSpace β] [Fintype β] (w : β → ENNReal) :
Measure β

The measure on a finite type giving each point its weight.

Equations
Instances For
    source
    @[simp]
    theorem MeasureTheory.Measure.ofWeights_apply_singleton {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] (w : β → ENNReal) (b : β) :
    (ofWeights w) {b} = w b
    source
    theorem MeasureTheory.Measure.ofWeights_apply_singleton_ne_zero {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] {w : β → ENNReal} {b : β} (h : w b ≠ 0) :
    (ofWeights w) {b} ≠ 0
    source
    theorem MeasureTheory.Measure.ofWeights_apply_finset {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] (w : β → ENNReal) (s : Finset β) :
    (ofWeights w) ↑s = ∑ b ∈ s, w b

    The weight measure of a finite set is the sum of its points' weights.

    source
    theorem MeasureTheory.Measure.isFiniteMeasure_ofWeights {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] {w : β → ENNReal} (hw : ∀ (b : β), w b ≠ ⊤) :
    IsFiniteMeasure (ofWeights w)

    Finite weights give a finite measure.

    source
    instance MeasureTheory.Measure.instIsFiniteMeasureOfWeightsCastENNReal {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] (w : β → ℕ) :
    IsFiniteMeasure (ofWeights fun (b : β) => ↑(w b))