Dirac measure #

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

The dirac measure.

  • One or more equations did not get rendered due to their size.
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) :
    theorem MeasureTheory.Measure.map_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (c : β) : (fun (x : α) => c) μ = μ Set.univ MeasureTheory.Measure.dirac c

    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

    Extra instances to short-circuit type class resolution