# 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.

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

The dirac measure.

Instances For
theorem MeasureTheory.Measure.le_dirac_apply {α : Type u_1} [] {s : Set α} {a : α} :
s
@[simp]
theorem MeasureTheory.Measure.dirac_apply' {α : Type u_1} [] {s : Set α} (a : α) (hs : ) :
s =
@[simp]
theorem MeasureTheory.Measure.dirac_apply_of_mem {α : Type u_1} [] {s : Set α} {a : α} (h : a s) :
s = 1
@[simp]
theorem MeasureTheory.Measure.dirac_apply {α : Type u_1} [] (a : α) (s : Set α) :
s =
theorem MeasureTheory.Measure.map_dirac {α : Type u_2} {β : Type u_1} [] [] {f : αβ} (hf : ) (a : α) :
@[simp]
theorem MeasureTheory.Measure.restrict_singleton {α : Type u_1} [] (μ : ) (a : α) :
= μ {a}
theorem MeasureTheory.Measure.map_eq_sum {α : Type u_2} {β : Type u_1} [] [] [] (μ : ) (f : αβ) (hf : ) :
= MeasureTheory.Measure.sum fun b => μ (f ⁻¹' {b})

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

@[simp]
theorem MeasureTheory.Measure.sum_smul_dirac {α : Type u_1} [] [] (μ : ) :
(MeasureTheory.Measure.sum fun a => μ {a} ) = μ

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

theorem MeasureTheory.Measure.tsum_indicator_apply_singleton {α : Type u_1} [] [] (μ : ) (s : Set α) (hs : ) :
∑' (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.mem_ae_dirac_iff {α : Type u_1} [] {s : Set α} {a : α} (hs : ) :
theorem MeasureTheory.ae_dirac_iff {α : Type u_1} [] {a : α} {p : αProp} (hp : MeasurableSet {x | p x}) :
(∀ᵐ (x : α) ∂, p x) p a
@[simp]
theorem MeasureTheory.ae_dirac_eq {α : Type u_1} [] (a : α) :
theorem MeasureTheory.ae_eq_dirac' {α : Type u_2} {β : Type u_1} [] [] {a : α} {f : αβ} (hf : ) :
theorem MeasureTheory.ae_eq_dirac {α : Type u_2} [] {δ : Type u_1} {a : α} (f : αδ) :
theorem MeasureTheory.restrict_dirac' {α : Type u_1} [] {s : Set α} {a : α} (hs : ) [Decidable (a s)] :
= if a s then else 0
theorem MeasureTheory.restrict_dirac {α : Type u_1} [] {s : Set α} {a : α} [Decidable (a s)] :
= if a s then else 0