Dirac measure #

In this file we define the Dirac measure MeasureTheory.Measure.dirac a and prove some basic facts about it.

The dirac measure.

Instances For
    theorem MeasureTheory.Measure.dirac_apply' {α : Type u_1} [MeasurableSpace α] {s : Set α} (a : α) (hs : MeasurableSet s) :
    theorem MeasureTheory.Measure.dirac_apply_of_mem {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} (h : a s) :

    If f is a map with countable codomain, then μ.map f is a sum of Dirac measures.


    A measure on a countable type is a sum of Dirac measures.

    theorem MeasureTheory.Measure.tsum_indicator_apply_singleton {α : Type u_1} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) (s : Set α) (hs : MeasurableSet s) :
    ∑' (x : α), Set.indicator s (fun x => μ {x}) x = μ s

    Given that α is a countable, measurable space with all singleton sets measurable, write the measure of a set s as the sum of the measure of {x} for all x ∈ s.

    theorem MeasureTheory.ae_dirac_iff {α : Type u_1} [MeasurableSpace α] {a : α} {p : αProp} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ (x : α) ∂MeasureTheory.Measure.dirac a, p x) p a