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.

@[simp]
theorem MeasureTheory.Measure.dirac_apply' {α : Type u_1} [MeasurableSpace α] {s : Set α} (a : α) (hs : MeasurableSet s) :
@[simp]
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 : β) :
MeasureTheory.Measure.map (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.

@[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 : α), 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