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
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.Measure.le_dirac_apply
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
{a : α}
:
Set.indicator s 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 = Set.indicator s 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 = Set.indicator s 1 a
theorem
MeasureTheory.Measure.map_dirac
{α : Type u_2}
{β : Type u_1}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : Measurable f)
(a : α)
:
@[simp]
theorem
MeasureTheory.Measure.restrict_singleton
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
(a : α)
:
MeasureTheory.Measure.restrict μ {a} = ↑↑μ {a} • MeasureTheory.Measure.dirac a
theorem
MeasureTheory.Measure.map_eq_sum
{α : Type u_2}
{β : Type u_1}
[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 : α), 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}
[MeasurableSpace α]
{s : Set α}
{a : α}
(hs : MeasurableSet s)
:
s ∈ MeasureTheory.Measure.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 : α)
:
theorem
MeasureTheory.ae_eq_dirac'
{α : Type u_2}
{β : Type u_1}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass β]
{a : α}
{f : α → β}
(hf : Measurable f)
:
theorem
MeasureTheory.ae_eq_dirac
{α : Type u_2}
[MeasurableSpace α]
{δ : Type u_1}
[MeasurableSingletonClass α]
{a : α}
(f : α → δ)
:
theorem
MeasureTheory.restrict_dirac'
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
{a : α}
(hs : MeasurableSet s)
[Decidable (a ∈ s)]
:
MeasureTheory.Measure.restrict (MeasureTheory.Measure.dirac a) 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.restrict (MeasureTheory.Measure.dirac a) s = if a ∈ s then MeasureTheory.Measure.dirac a else 0