Theorems · Theorem · measure theory

HasSum.isProbabilityMeasure_sum_dirac

∀ {δ : Type u_3} {ι : Type u_4} {mδ : MeasurableSpace δ} {c : ι → ℝ} {d : ι → δ},
  (∀ (i : ι), 0 ≤ c i) →
    HasSum c 1 →
      MeasureTheory.IsProbabilityMeasure
        (MeasureTheory.Measure.sum fun i => ENNReal.ofReal (c i) • MeasureTheory.Measure.dirac (d i))

Defined in: Mathlib.MeasureTheory.Measure.Dirac
Cited by: 0 results in Mathlib
Foundations: Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement · cited by 9,879
SummationFilter.unconditionalstatement and proof · cited by 2,068
ENNReal.ofRealstatement · cited by 863
HasSumstatement and proof · cited by 518
MeasureTheory.IsProbabilityMeasurestatement · cited by 392
Real.toNNRealproof · cited by 267
MeasureTheory.Measure.diracstatement · cited by 210
MeasureTheory.Measure.sumstatement · cited by 121
Real.toNNReal_oneproof · cited by 13

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.