Theorems · Theorem · probability
ProbabilityTheory.IsGaussian.noAtoms
Deprecated since 2026-06-09Use ProbabilityTheory.IsGaussian.nullSingletonClass instead.
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
{μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
(∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x) → MeasureTheory.NullSingletonClass μAlias of ProbabilityTheory.IsGaussian.nullSingletonClass.
If a Gaussian measure is not a Dirac, then it has value zero on singletons.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 314 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- NormedAddCommGroupstatement · cited by 15,752
- MeasurableSpacestatement · cited by 13,106
- NormedSpacestatement · cited by 12,499
- MeasureTheory.Measurestatement · cited by 10,939
- CompleteSpacestatement · cited by 2,532
- BorelSpacestatement · cited by 1,602
- SecondCountableTopologystatement · cited by 750
- MeasureTheory.Measure.diracstatement · cited by 210
- MeasureTheory.NullSingletonClassstatement · cited by 125
- ProbabilityTheory.IsGaussianstatement · cited by 48
- ProbabilityTheory.IsGaussian.nullSingletonClassproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.