Documentation

Mathlib.MeasureTheory.Measure.Dirac

Dirac measure #

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

The dirac measure.

Equations
Instances For
    theorem MeasureTheory.Measure.le_dirac_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} :
    s.indicator 1 a (MeasureTheory.Measure.dirac a) s
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply' {α : Type u_1} [MeasurableSpace α] {s : Set α} (a : α) (hs : MeasurableSet s) :
    (MeasureTheory.Measure.dirac a) s = s.indicator 1 a
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply_of_mem {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} (h : a s) :
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Set α) :
    (MeasureTheory.Measure.dirac a) s = s.indicator 1 a
    theorem MeasureTheory.Measure.map_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (c : β) :
    MeasureTheory.Measure.map (fun (x : α) => c) μ = μ Set.univ MeasureTheory.Measure.dirac c
    @[simp]
    theorem MeasureTheory.Measure.restrict_singleton {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (a : α) :
    μ.restrict {a} = μ {a} MeasureTheory.Measure.dirac a

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

    @[simp]

    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 : α), s.indicator (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
    theorem MeasureTheory.ae_eq_dirac' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {a : α} {f : αβ} (hf : Measurable f) :
    theorem MeasureTheory.ae_eq_dirac {α : Type u_1} {δ : Type u_3} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} (f : αδ) :

    Extra instances to short-circuit type class resolution

    theorem MeasureTheory.restrict_dirac' {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} (hs : MeasurableSet s) [Decidable (a s)] :
    (MeasureTheory.Measure.dirac a).restrict s = if a s then MeasureTheory.Measure.dirac a else 0
    theorem MeasureTheory.restrict_dirac {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} [MeasurableSingletonClass α] [Decidable (a s)] :
    (MeasureTheory.Measure.dirac a).restrict s = if a s then MeasureTheory.Measure.dirac a else 0

    Dirac delta measures at two points are equal if every measurable set contains either both or neither of the points.

    Dirac delta measures at two points are different if and only if there is a measurable set containing one of the points but not the other.

    Dirac delta measures at two different points are different, assuming the measurable space separates points.

    Dirac delta measures at two points are different if and only if the two points are different, assuming the measurable space separates points.

    Dirac delta measures at two points are equal if and only if the two points are equal, assuming the measurable space separates points.

    The assignment x ↦ dirac x is injective, assuming the measurable space separates points.