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} [MeasurableSpace α] (a : α) : MeasureTheory.Measure α

The dirac measure.

Equations

• MeasureTheory.Measure.dirac a = (MeasureTheory.OuterMeasure.dirac a).toMeasure ⋯

instance MeasureTheory.Measure.instMeasureSpacePUnit : MeasureTheory.MeasureSpace PUnit.{u_4 + 1}

Equations

• MeasureTheory.Measure.instMeasureSpacePUnit = MeasureTheory.MeasureSpace.mk (MeasureTheory.Measure.dirac PUnit.unit)

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) : (MeasureTheory.Measure.dirac a) s = 1

@[simp]

theorem MeasureTheory.Measure.dirac_apply {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Set α) : (MeasureTheory.Measure.dirac a) s = s.indicator 1 a

@[simp]

theorem MeasureTheory.Measure.dirac_ne_zero {α : Type u_1} [MeasurableSpace α] {a : α} : MeasureTheory.Measure.dirac a ≠ 0

theorem MeasureTheory.Measure.map_dirac {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Measurable f) (a : α) : MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f 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

theorem MeasureTheory.Measure.ext_of_singleton {α : Type u_1} [MeasurableSpace α] [Countable α] {μ ν : MeasureTheory.Measure α} (h : ∀ (a : α), μ {a} = ν {a}) : μ = ν

Two measures on a countable space are equal if they agree on singletons.

theorem MeasureTheory.Measure.ext_iff_singleton {α : Type u_1} [MeasurableSpace α] [Countable α] {μ ν : MeasureTheory.Measure α} : μ = ν ↔ ∀ (a : α), μ {a} = ν {a}

Two measures on a countable space are equal if and only if they agree on singletons.

theorem MeasureTheory.Measure.map_eq_sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure α) (f : α → β) (hf : Measurable f) : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.sum fun (b : β) => μ (f ⁻¹' {b}) • MeasureTheory.Measure.dirac 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} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) : (MeasureTheory.Measure.sum fun (a : α) => μ {a} • MeasureTheory.Measure.dirac a) = μ

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.mem_ae_dirac_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} {a : α} (hs : MeasurableSet s) : s ∈ MeasureTheory.ae (MeasureTheory.Measure.dirac a) ↔ a ∈ 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

@[simp]

theorem MeasureTheory.ae_dirac_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) : MeasureTheory.ae (MeasureTheory.Measure.dirac a) = pure a

theorem MeasureTheory.ae_eq_dirac' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {a : α} {f : α → β} (hf : Measurable f) : f =ᵐ[MeasureTheory.Measure.dirac a] Function.const α (f a)

theorem MeasureTheory.ae_eq_dirac {α : Type u_1} {δ : Type u_3} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} (f : α → δ) : f =ᵐ[MeasureTheory.Measure.dirac a] Function.const α (f a)

instance MeasureTheory.Measure.dirac.isProbabilityMeasure {α : Type u_1} [MeasurableSpace α] {x : α} : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.dirac x)

Equations

• ⋯ = ⋯

Extra instances to short-circuit type class resolution

instance MeasureTheory.Measure.dirac.instIsFiniteMeasure {α : Type u_1} [MeasurableSpace α] {a : α} : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.dirac a)

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.dirac.instSigmaFinite {α : Type u_1} [MeasurableSpace α] {a : α} : MeasureTheory.SigmaFinite (MeasureTheory.Measure.dirac a)

Equations

• ⋯ = ⋯

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

theorem MeasureTheory.mutuallySingular_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (x : α) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : (MeasureTheory.Measure.dirac x).MutuallySingular μ

theorem MeasureTheory.dirac_eq_dirac_iff_forall_mem_iff_mem {α : Type u_1} [MeasurableSpace α] {x y : α} : MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)

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

theorem MeasureTheory.dirac_ne_dirac_iff_exists_measurableSet {α : Type u_1} [MeasurableSpace α] {x y : α} : MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ ∃ (A : Set α), MeasurableSet A ∧ x ∈ A ∧ y ∉ A

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.

theorem MeasureTheory.dirac_ne_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α} (x_ne_y : x ≠ y) : MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y

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

theorem MeasureTheory.dirac_ne_dirac_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α} : MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ x ≠ y

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

theorem MeasureTheory.dirac_eq_dirac_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α} : MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y ↔ x = y

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

theorem MeasureTheory.injective_dirac {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] : Function.Injective fun (x : α) => MeasureTheory.Measure.dirac x

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