English
There exists a representation of any countable-measure μ as a sum of Dirac measures with appropriate weights.
Русский
Существует представление меры μ на счётном множестве в виде суммы мер Дирака с соответствующими весами.
LaTeX
$$$ ∃ s ⊆ α,\ μ = \\sum x ∈ s \\; μ(\\{x\\}) · dirac x $$$
Lean4
/-- A measure on a countable type is a sum of Dirac measures.
If `α` has measurable singletons, `sum_smul_dirac` gives a simpler sum. -/
theorem exists_sum_smul_dirac [Countable α] (μ : Measure α) :
∃ s : Set α, μ = Measure.sum (fun x : s ↦ μ (measurableAtom x) • dirac (x : α)) :=
by
let measurableAtoms := measurableAtom '' (Set.univ : Set α)
have h_nonempty (s : measurableAtoms) : Set.Nonempty s.1 :=
by
obtain ⟨y, _, hy⟩ := s.2
rw [← hy]
exact ⟨y, mem_measurableAtom_self y⟩
let points : measurableAtoms → α := fun s ↦ (h_nonempty s).some
have h_points_mem (s : measurableAtoms) : points s ∈ s.1 := (h_nonempty s).some_mem
refine ⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩
rw [sum_apply _ (MeasurableSet.measurableAtom_of_countable x)]
simp only [Measure.smul_apply, smul_eq_mul]
simp_rw [dirac_apply' _ (MeasurableSet.measurableAtom_of_countable x)]
rw [tsum_eq_single ⟨points ⟨measurableAtom x, by simp [measurableAtoms]⟩, by simp⟩]
· rw [indicator_of_mem]
· simp only [Pi.one_apply, mul_one]
congr 1
refine (measurableAtom_eq_of_mem ?_).symm
convert h_points_mem _
simp
· convert h_points_mem _
simp
· simp only [ne_eq, mul_eq_zero, indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false, Subtype.forall,
Set.mem_range, Subtype.exists, Subtype.mk.injEq, forall_exists_index]
refine fun y s hs hsy hyx ↦ .inr fun hyx' ↦ hyx ?_
rw [← hsy]
congr
have h1 : measurableAtom y = measurableAtom x := measurableAtom_eq_of_mem hyx'
have h2 : measurableAtom y = s := by
specialize h_points_mem ⟨s, hs⟩
obtain ⟨z, _, hz⟩ := hs
simp only at h_points_mem
rw [← hz, ← hsy]
refine measurableAtom_eq_of_mem ?_
convert h_points_mem
rw [← h2, h1]
