Haar measures without atoms #
σ-finite, inner regular Haar measures on non-discrete groups have no atoms. In particular, this
gives NoAtoms' instances for additive Haar measures on finite-dimensional real vector spaces
and for the Lebesgue measure on the unit interval.
theorem MeasureTheory.NoAtoms'.of_isHaarMeasure {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [IsTopologicalGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 1 {1}ᶜ).NeBot] (μ : Measure G) [μ.IsHaarMeasure] [μ.InnerRegularCompactLTTop] [SigmaFinite μ] :
NoAtoms' μ
Analogue of MeasureTheory.Measure.IsHaarMeasure.nullSingletonClass for NoAtoms'.
Without σ-finiteness, this fails: for the Haar measure on ℝ × ℝ_discrete, the set
{0} × ℝ_discrete is an atom of infinite measure.
theorem MeasureTheory.NoAtoms'.of_isAddHaarMeasure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 0 {0}ᶜ).NeBot] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.InnerRegularCompactLTTop] [SigmaFinite μ] :
NoAtoms' μ
Analogue of MeasureTheory.Measure.IsAddHaarMeasure.nullSingletonClass for NoAtoms'.
Without σ-finiteness, this fails: for the Haar measure on ℝ × ℝ_discrete, the set
{0} × ℝ_discrete is an atom of infinite measure.
instance MeasureTheory.NoAtoms'.instOfBorelSpaceOfFiniteDimensionalRealOfIsAddHaarMeasureOfNontrivial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] :
NoAtoms' μ