refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): rename NoAtoms to NullSingletonClass

Counterexamples/Phillips.lean

@@ -432,7 +432,7 @@ theorem toFunctions_toMeasure [MeasurableSpace α] (μ : Measure α) [IsFiniteMe
 
 set_option backward.isDefEq.respectTransparency false in
 theorem toFunctions_toMeasure_continuousPart [MeasurableSpace α] [MeasurableSingletonClass α]
-    (μ : Measure α) [IsFiniteMeasure μ] [NoAtoms μ] (s : Set α) (hs : MeasurableSet s) :
+    (μ : Measure α) [IsFiniteMeasure μ] [NullSingletonClass μ] (s : Set α) (hs : MeasurableSet s) :
     μ.extensionToBoundedFunctions.toBoundedAdditiveMeasure.continuousPart s = μ.real s := by
   let f := μ.extensionToBoundedFunctions.toBoundedAdditiveMeasure
   change f (univ \ f.discreteSupport ∩ s) = μ.real s

Mathlib.lean

@@ -5588,7 +5588,7 @@ public import Mathlib.MeasureTheory.Measure.TightNormed
 public import Mathlib.MeasureTheory.Measure.Tilted
 public import Mathlib.MeasureTheory.Measure.Trim
 public import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
-public import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
+public import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
 public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
 public import Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
 public import Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Mathlib/Analysis/Convolution.lean

@@ -946,7 +946,7 @@ noncomputable def posConvolution (f : ℝ → E) (g : ℝ → E') (L : E →L[
   indicator (Ioi (0 : ℝ)) fun x => ∫ t in 0..x, L (f t) (g (x - t)) ∂ν
 
 theorem posConvolution_eq_convolution_indicator (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F)
-    (ν : Measure ℝ := by volume_tac) [NoAtoms ν] :
+    (ν : Measure ℝ := by volume_tac) [NullSingletonClass ν] :
     posConvolution f g L ν = convolution (indicator (Ioi 0) f) (indicator (Ioi 0) g) L ν := by
   ext1 x
   rw [convolution, posConvolution, indicator]
@@ -974,7 +974,7 @@ theorem posConvolution_eq_convolution_indicator (f : ℝ → E) (g : ℝ → E')
     · rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, zero_apply]
 
 theorem integrable_posConvolution {f : ℝ → E} {g : ℝ → E'} {μ ν : Measure ℝ} [SFinite μ]
-    [SFinite ν] [IsAddRightInvariant μ] [NoAtoms ν] (hf : IntegrableOn f (Ioi 0) ν)
+    [SFinite ν] [IsAddRightInvariant μ] [NullSingletonClass ν] (hf : IntegrableOn f (Ioi 0) ν)
     (hg : IntegrableOn g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F) :
     Integrable (posConvolution f g L ν) μ := by
   rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))] at hf hg
@@ -985,7 +985,7 @@ theorem integrable_posConvolution {f : ℝ → E} {g : ℝ → E'} {μ ν : Meas
 of their integrals over this set. (Compare `integral_convolution` for the two-sided convolution.) -/
 theorem integral_posConvolution [CompleteSpace E] [CompleteSpace E'] [CompleteSpace F]
     {μ ν : Measure ℝ}
-    [SFinite μ] [SFinite ν] [IsAddRightInvariant μ] [NoAtoms ν] {f : ℝ → E} {g : ℝ → E'}
+    [SFinite μ] [SFinite ν] [IsAddRightInvariant μ] [NullSingletonClass ν] {f : ℝ → E} {g : ℝ → E'}
     (hf : IntegrableOn f (Ioi 0) ν) (hg : IntegrableOn g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F) :
     ∫ x : ℝ in Ioi 0, ∫ t : ℝ in 0..x, L (f t) (g (x - t)) ∂ν ∂μ =
       L (∫ x : ℝ in Ioi 0, f x ∂ν) (∫ x : ℝ in Ioi 0, g x ∂μ) := by

Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
 public import Mathlib.MeasureTheory.MeasurableSpace.Prod
-public import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
+public import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
 public import Mathlib.Topology.Instances.Real.Lemmas
 
 /-!
@@ -573,7 +573,7 @@ lemma tendsto_measure_Icc_nhdsWithin_right (b : ℝ) :
   intro s hs
   simpa using mem_of_mem_nhds hs
 
-lemma tendsto_measure_Icc [NoAtoms μ] (b : ℝ) :
+lemma tendsto_measure_Icc [NullSingletonClass μ] (b : ℝ) :
     Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝 (0 : ℝ)) (𝓝 0) := by
   rw [← nhdsLT_sup_nhdsGE, tendsto_sup]
   constructor

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -410,11 +410,12 @@ lemma _root_.MeasureTheory.measurePreserving_eval [∀ i, IsProbabilityMeasure (
   rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
   exact fun _ _ ↦ measure_univ
 
-theorem pi_hyperplane (i : ι) [NoAtoms (μ i)] (x : α i) :
+theorem pi_hyperplane (i : ι) [NullSingletonClass (μ i)] (x : α i) :
     Measure.pi μ { f : ∀ i, α i | f i = x } = 0 :=
   show Measure.pi μ (eval i ⁻¹' {x}) = 0 from pi_eval_preimage_null _ (measure_singleton x)
 
-theorem ae_eval_ne (i : ι) [NoAtoms (μ i)] (x : α i) : ∀ᵐ y : ∀ i, α i ∂Measure.pi μ, y i ≠ x :=
+theorem ae_eval_ne (i : ι) [NullSingletonClass (μ i)] (x : α i) :
+    ∀ᵐ y : ∀ i, α i ∂Measure.pi μ, y i ≠ x :=
   compl_mem_ae_iff.2 (pi_hyperplane μ i x)
 
 theorem restrict_pi_pi (s : (i : ι) → Set (α i)) :
@@ -467,7 +468,7 @@ lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpac
 
 section Intervals
 
-variable [∀ i, PartialOrder (α i)] [∀ i, NoAtoms (μ i)]
+variable [∀ i, PartialOrder (α i)] [∀ i, NullSingletonClass (μ i)]
 
 theorem pi_Iio_ae_eq_pi_Iic {s : Set ι} {f : ∀ i, α i} :
     (pi s fun i => Iio (f i)) =ᵐ[Measure.pi μ] pi s fun i => Iic (f i) :=
@@ -515,18 +516,27 @@ theorem univ_pi_Ico_ae_eq_Icc {f g : ∀ i, α i} :
 
 end Intervals
 
-/-- If one of the measures `μ i` has no atoms, them `Measure.pi µ`
-has no atoms. The instance below assumes that all `μ i` have no atoms. -/
-theorem pi_noAtoms (i : ι) [NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
+/-- If one of the measures `μ i` has value zero on singeltons, them `Measure.pi µ`
+has value zero on singletons. The instance below assumes that all `μ i` have value zero on
+singletons. -/
+theorem pi_nullSingletonClass (i : ι) [NullSingletonClass (μ i)] :
+    NullSingletonClass (Measure.pi μ) :=
   ⟨fun x => flip measure_mono_null (pi_hyperplane μ i (x i)) (singleton_subset_iff.2 rfl)⟩
 
-instance pi_noAtoms' [h : Nonempty ι] [∀ i, NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
-  h.elim fun i => pi_noAtoms i
+@[deprecated (since := "2026-06-09")]
+alias pi_noAtoms := pi_nullSingletonClass
+
+instance pi_nullSingletonClass' [h : Nonempty ι] [∀ i, NullSingletonClass (μ i)] :
+    NullSingletonClass (Measure.pi μ) :=
+  h.elim fun i => pi_nullSingletonClass i
+
+@[deprecated (since := "2026-06-09")]
+alias pi_noAtoms' := pi_nullSingletonClass'
 
 instance {α : ι → Type*} [Nonempty ι] [∀ i, MeasureSpace (α i)]
-    [∀ i, SigmaFinite (volume : Measure (α i))] [∀ i, NoAtoms (volume : Measure (α i))] :
-    NoAtoms (volume : Measure (∀ i, α i)) :=
-  pi_noAtoms'
+    [∀ i, SigmaFinite (volume : Measure (α i))] [∀ i, NullSingletonClass (volume : Measure (α i))] :
+    NullSingletonClass (volume : Measure (∀ i, α i)) :=
+  pi_nullSingletonClass'
 
 instance pi.isLocallyFiniteMeasure
     [∀ i, TopologicalSpace (α i)] [∀ i, IsLocallyFiniteMeasure (μ i)] :

Mathlib/MeasureTheory/Constructions/UnitInterval.lean

@@ -11,7 +11,7 @@ public import Mathlib.MeasureTheory.Measure.Haar.Unique
 # The canonical measure on the unit interval
 
 This file provides a `MeasureTheory.MeasureSpace` instance on `unitInterval`,
-and shows it is a probability measure with no atoms.
+and shows it is a probability measure with value zero on singletons.
 
 It also contains some basic results on the volume of various interval sets.
 -/
@@ -43,7 +43,7 @@ lemma volume_apply {s : Set I} : volume s = volume (Subtype.val '' s) :=
 lemma measurePreserving_coe : MeasurePreserving ((↑) : I → ℝ) volume (volume.restrict I) :=
   measurePreserving_subtype_coe measurableSet_Icc
 
-instance : NoAtoms (volume : Measure I) where
+instance : NullSingletonClass (volume : Measure I) where
   measure_singleton x := by simp [volume_apply]
 
 @[fun_prop]

Mathlib/MeasureTheory/Group/Measure.lean

@@ -918,20 +918,20 @@ instance prod.instIsHaarMeasure {G : Type*} [Group G] [TopologicalSpace G] {_ :
     (ν : Measure H) [IsHaarMeasure μ] [IsHaarMeasure ν] [SFinite μ] [SFinite ν]
     [MeasurableMul G] [MeasurableMul H] : IsHaarMeasure (μ.prod ν) where
 
-/-- If the neutral element of a group is not isolated, then a Haar measure on this group has
-no atoms.
+/-- If the neutral element of a group is not isolated, then a Haar measure on this group has value
+zero on singletons.
 
 The additive version of this instance applies in particular to show that an additive Haar
 measure on a nontrivial finite-dimensional real vector space has no atom. -/
 @[to_additive
 /-- If the zero element of an additive group is not isolated, then an additive Haar measure on this
-group has no atoms.
+group has value zero on singletons.
 
 This applies in particular to show that an additive Haar measure on a nontrivial
 finite-dimensional real vector space has no atom. -/]
-instance (priority := 100) IsHaarMeasure.noAtoms [IsTopologicalGroup G] [BorelSpace G] [T1Space G]
-    [WeaklyLocallyCompactSpace G] [(𝓝[≠] (1 : G)).NeBot] (μ : Measure G) [μ.IsHaarMeasure] :
-    NoAtoms μ := by
+instance (priority := 100) IsHaarMeasure.nullSingletonClass [IsTopologicalGroup G] [BorelSpace G]
+    [T1Space G] [WeaklyLocallyCompactSpace G] [(𝓝[≠] (1 : G)).NeBot] (μ : Measure G)
+    [μ.IsHaarMeasure] : NullSingletonClass μ := by
   cases eq_or_ne (μ 1) 0 with
   | inl h => constructor; simpa
   | inr h =>
@@ -940,6 +940,9 @@ instance (priority := 100) IsHaarMeasure.noAtoms [IsTopologicalGroup G] [BorelSp
     exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
       K_compact.measure_lt_top.ne
 
+@[deprecated (since := "2026-06-09")]
+alias IsHaarMeasure.noAtoms := IsHaarMeasure.nullSingletonClass
+
 instance IsAddHaarMeasure.domSMul {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A]
     [MeasurableSpace A] [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A]
     [ContinuousConstSMul G A] {μ : Measure A} [μ.IsAddHaarMeasure] (g : Gᵈᵐᵃ) :

Mathlib/MeasureTheory/Integral/Bochner/Set.lean

@@ -666,7 +666,7 @@ theorem setIntegral_trim {X} {m m0 : MeasurableSpace X} {μ : Measure X} (hm : m
 /-! ### Lemmas about adding and removing interval boundaries
 
 The primed lemmas take explicit arguments about the endpoint having zero measure, while the
-unprimed ones use `[NoAtoms μ]`.
+unprimed ones use `[NullSingletonClass μ]`.
 -/
 
 section PartialOrder
@@ -701,7 +701,7 @@ theorem integral_Ici_eq_integral_Ioi' (hx : μ {x} = 0) :
     ∫ t in Ici x, f t ∂μ = ∫ t in Ioi x, f t ∂μ :=
   setIntegral_congr_set (Ioi_ae_eq_Ici' hx).symm
 
-variable [NoAtoms μ]
+variable [NullSingletonClass μ]
 
 theorem integral_Icc_eq_integral_Ioc : ∫ t in Icc x y, f t ∂μ = ∫ t in Ioc x y, f t ∂μ :=
   integral_Icc_eq_integral_Ioc' <| measure_singleton x

Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

@@ -435,7 +435,7 @@ theorem continuousAt_parametric_primitive_of_dominated [FirstCountableTopology X
     rw [nhds_prod_eq]
     exact (continuous_abs.tendsto' _ _ abs_zero).comp (this.comp tendsto_snd)
 
-variable [NoAtoms μ]
+variable [NullSingletonClass μ]
 
 theorem continuousOn_primitive (h_int : IntegrableOn f (Icc a b) μ) :
     ContinuousOn (fun x => ∫ t in Ioc a x, f t ∂μ) (Icc a b) := by
@@ -636,8 +636,8 @@ theorem continuousWithinAt_Ici_primitive_Ioi {a₀ : ℝ} (hf : IntegrableOn f (
     · filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_mem_nhds hx)] with a ha using by grind
     · filter_upwards [self_mem_nhdsWithin] with a ha using by grind
 
-theorem continuousOn_Ici_primitive_Ioi [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Ioi a₀) μ) :
-    ContinuousOn (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) := by
+theorem continuousOn_Ici_primitive_Ioi [NullSingletonClass μ] {a₀ : ℝ}
+    (hf : IntegrableOn f (Ioi a₀) μ) : ContinuousOn (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) := by
   intro a (ha : a₀ ≤ a)
   rw [continuousWithinAt_iff_continuous_left_right]
   constructor
@@ -671,8 +671,8 @@ theorem continuousWithinAt_Iic_primitive_Iio {a₀ : ℝ} (hf : IntegrableOn f (
     · filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind
     · filter_upwards [self_mem_nhdsWithin] with a ha using by grind
 
-theorem continuousOn_Iic_primitive_Iio [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Iio a₀) μ) :
-    ContinuousOn (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) := by
+theorem continuousOn_Iic_primitive_Iio [NullSingletonClass μ] {a₀ : ℝ}
+    (hf : IntegrableOn f (Iio a₀) μ) : ContinuousOn (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) := by
   intro a (ha : a ≤ a₀)
   rw [continuousWithinAt_iff_continuous_left_right]
   constructor
@@ -688,13 +688,13 @@ theorem continuousOn_Iic_primitive_Iio [NoAtoms μ] {a₀ : ℝ} (hf : Integrabl
       continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
     exact (continuousWithinAt_const.add h_cwa).congr h_split (h_split a (left_mem_Icc.2 ha))
 
-theorem continuousOn_Ici_primitive_Ici [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Ici a₀) μ) :
-    ContinuousOn (fun b ↦ ∫ x in Ici b, f x ∂μ) (Ici a₀) := by
+theorem continuousOn_Ici_primitive_Ici [NullSingletonClass μ] {a₀ : ℝ}
+    (hf : IntegrableOn f (Ici a₀) μ) : ContinuousOn (fun b ↦ ∫ x in Ici b, f x ∂μ) (Ici a₀) := by
   simp_rw [integral_Ici_eq_integral_Ioi]
   exact (hf.mono_set Ioi_subset_Ici_self).continuousOn_Ici_primitive_Ioi
 
-theorem continuousOn_Iic_primitive_Iic [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Iic a₀) μ) :
-    ContinuousOn (fun b ↦ ∫ x in Iic b, f x ∂μ) (Iic a₀) := by
+theorem continuousOn_Iic_primitive_Iic [NullSingletonClass μ] {a₀ : ℝ}
+    (hf : IntegrableOn f (Iic a₀) μ) : ContinuousOn (fun b ↦ ∫ x in Iic b, f x ∂μ) (Iic a₀) := by
   simp_rw [integral_Iic_eq_integral_Iio]
   exact (hf.mono_set Iio_subset_Iic_self).continuousOn_Iic_primitive_Iio
 

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -850,7 +850,7 @@ theorem ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin {α β : Type*} [Meas
 /-! ### Lemmas about adding and removing interval boundaries
 
 The primed lemmas take explicit arguments about the measure being finite at the endpoint, while
-the unprimed ones use `[NoAtoms μ]`.
+the unprimed ones use `[NullSingletonClass μ]`.
 -/
 
 
@@ -908,7 +908,7 @@ theorem integrableOn_Iic_iff_integrableOn_Iio'
     IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ := by
   rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
 
-variable [NoAtoms μ]
+variable [NullSingletonClass μ]
 
 theorem integrableOn_Icc_iff_integrableOn_Ioc (ha : ‖f a‖ₑ ≠ ∞ := by finiteness) :
     IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ :=

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -247,7 +247,7 @@ include ha hb in
 theorem aecover_Ioo_of_Ioc : AECover (μ.restrict <| Ioo A B) l fun i => Ioc (a i) (b i) :=
   (aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Ioc_self) fun _ ↦ measurableSet_Ioc
 
-variable [NoAtoms μ]
+variable [NullSingletonClass μ]
 
 theorem aecover_Ioc_of_Icc (ha : Tendsto a l (𝓝 A)) (hb : Tendsto b l (𝓝 B)) :
     AECover (μ.restrict <| Ioc A B) l fun i => Icc (a i) (b i) :=

Mathlib/MeasureTheory/Integral/IntervalAverage.lean

@@ -19,7 +19,7 @@ formulas for this average:
 * `interval_average_eq_div`: `⨍ x in a..b, f x = (∫ x in a..b, f x) / (b - a)`;
 * `exists_eq_interval_average_of_measure`:
     `∃ c ∈ Ι a b, f c = ⨍ x in Ι a b, f x ∂μ`.
-* `exists_eq_interval_average_of_noAtoms`:
+* `exists_eq_interval_average_of_nullSingletonClass`:
     `∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ`.
 * `exists_eq_interval_average`:
     `∃ c ∈ uIoo a b, f c = ⨍ x in a..b, f x`.
@@ -78,10 +78,10 @@ theorem exists_eq_interval_average_of_measure
     isCompact_uIcc measurableSet_uIoc uIoc_subset_uIcc hμfin) hμfin hμ0
 
 /-- If `f : ℝ → ℝ` is continuous on `uIcc a b`, the interval has finite and nonzero `μ`-measure,
-and `μ` has no atoms, then `∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ`. -/
-theorem exists_eq_interval_average_of_noAtoms
-    [NoAtoms μ] (hf : ContinuousOn f (uIcc a b)) (hμfin : μ (Ι a b) ≠ ⊤) (hμ0 : μ (Ι a b) ≠ 0) :
-    ∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ := by
+and `μ` has value zero on singletons, then `∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ`. -/
+theorem exists_eq_interval_average_of_nullSingletonClass
+    [NullSingletonClass μ] (hf : ContinuousOn f (uIcc a b)) (hμfin : μ (Ι a b) ≠ ⊤)
+    (hμ0 : μ (Ι a b) ≠ 0) : ∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ := by
   have hint : IntegrableOn f (Ι a b) μ := hf.integrableOn_of_subset_isCompact
     isCompact_uIcc measurableSet_uIoc uIoc_subset_uIcc hμfin
   have h : a ≠ b := by intro hab; simp [hab] at hμ0
@@ -95,10 +95,14 @@ theorem exists_eq_interval_average_of_noAtoms
     (hint.mono_set hs') (measure_ne_top_of_subset hs' hμfin) hμ0'
   exact ⟨c, hc, by rwa [← setAverage_congr hs_ev]⟩
 
+@[deprecated (since := "2026-06-09")]
+alias exists_eq_interval_average_of_noAtoms := exists_eq_interval_average_of_nullSingletonClass
+
 /-- The mean value theorem for integrals:
 There exists a point in an interval such that the mean of a continuous function over the interval
 equals the value of the function at the point. -/
 theorem exists_eq_interval_average
     (hab : a ≠ b) (hf : ContinuousOn f (uIcc a b)) :
     ∃ c ∈ uIoo a b, f c = ⨍ x in a..b, f x :=
-  exists_eq_interval_average_of_noAtoms hf (by simp) (by simpa using sub_ne_zero.mpr hab.symm)
+  exists_eq_interval_average_of_nullSingletonClass hf (by simp)
+    (by simpa using sub_ne_zero.mpr hab.symm)