English
If a Gaussian measure is not a Dirac measure, it has no atoms.
Русский
Если гауссова мера не дираковская, то у неё нет атомов.
LaTeX
$$$(\\forall x, μ \\neq \\mathrm{dirac}(x)) \\Rightarrow NoAtoms(μ)$$$
Lean4
/-- If a Gaussian measure is not a Dirac, then it has no atoms. -/
theorem noAtoms (h : ∀ x, μ ≠ Measure.dirac x) : NoAtoms μ where
measure_singleton
x :=
by
obtain ⟨L, hL⟩ : ∃ L : StrongDual ℝ E, Var[L; μ] ≠ 0 :=
by
contrapose! h
exact ⟨_, eq_dirac_of_variance_eq_zero h⟩
have hL_zero : μ.map L {L x} = 0 :=
by
have : NoAtoms (μ.map L) := by
rw [map_eq_gaussianReal L]
refine noAtoms_gaussianReal ?_
simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm
rw [measure_singleton]
rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hL_zero
refine measure_mono_null ?_ hL_zero
exact fun ⦃a⦄ ↦ congrArg ⇑L
