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
- MeasureTheory.Measure.dirac a = (MeasureTheory.OuterMeasure.dirac a).toMeasure ⋯
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)
:
(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
theorem
MeasureTheory.Measure.map_dirac
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : Measurable 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.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.Measure.dirac a).ae ↔ 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.Measure.dirac a).ae = 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).ae] Function.const α (f a)
theorem
MeasureTheory.ae_eq_dirac
{α : Type u_1}
{δ : Type u_3}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{a : α}
(f : α → δ)
:
f =ᶠ[(MeasureTheory.Measure.dirac a).ae] Function.const α (f a)
instance
MeasureTheory.Measure.dirac.isProbabilityMeasure
{α : Type u_1}
[MeasurableSpace α]
{x : α}
:
Equations
- ⋯ = ⋯
Extra instances to short-circuit type class resolution
instance
MeasureTheory.Measure.dirac.instIsFiniteMeasure
{α : Type u_1}
[MeasurableSpace α]
{a : α}
:
Equations
- ⋯ = ⋯
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)
:
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 : α}
:
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 : α}
:
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.