Documentation

Mathlib.MeasureTheory.Measure.Dirac.Def

Dirac measure #

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

source
noncomputable def MeasureTheory.Measure.dirac {α : Type u_1} [MeasurableSpace α] (a : α) :
Measure α

The dirac measure.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance MeasureTheory.Measure.instMeasureSpacePUnit :
    MeasureSpace PUnit.{u_2 + 1}
    Equations
    source
    theorem MeasureTheory.Measure.le_dirac_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} :
    s.indicator 1 a ≤ (dirac a) s
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply' {α : Type u_1} [MeasurableSpace α] {s : Set α} (a : α) (hs : MeasurableSet s) :
    (dirac a) s = s.indicator 1 a
    source
    theorem MeasureTheory.Measure.dirac_apply_eq_zero_or_one {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} :
    (dirac a) s = 0 ∨ (dirac a) s = 1
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply_ne_zero_iff_eq_one {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} :
    (dirac a) s ≠ 0 ↔ (dirac a) s = 1
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply_ne_one_iff_eq_zero {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} :
    (dirac a) s ≠ 1 ↔ (dirac a) s = 0
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply_of_mem {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} (h : a ∈ s) :
    (dirac a) s = 1
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_real_apply_of_mem {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} (h : a ∈ s) :
    (dirac a).real s = 1
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_apply {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Set α) :
    (dirac a) s = s.indicator 1 a
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_real_apply {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Set α) :
    (dirac a).real s = s.indicator 1 a
    source
    @[simp]
    theorem MeasureTheory.Measure.dirac_ne_zero {α : Type u_1} [MeasurableSpace α] {a : α} :
    dirac a ≠ 0