MeasureTheory.NoAtoms

Stream: mathlib4

[Yongxi Lin (Aaron)]

I just realize that Mathlib's definition of NoAtoms is that the measure of each singleton is zero. I think this is really nonstandard and different from definitions I learnt in the past (i.e. ∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s). May I know the initial motivation for the design? Shall we change this definition? I think we should introduce the definition of Atoms (a measurable set that has positive measure and contains no set of smaller positive measures) and then use this definition to define atomic/nonatomic measures.

[Weiyi Wang]

Did some archeology and found it was introduced at https://github.com/leanprover-community/mathlib3/pull/3760. It has the comment "possibly should be redefined as ∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s." since the beginning and still has it as a TODO here

[Yongxi Lin (Aaron)]

I think I'll make a PR in the next several days. If NoAtoms is used for measures with atoms, how should I name the original typeclass for measures such that each singleton has measure zero? Maybe NullSingletonClass (as an extension of MeasurableSingletonClass)?