English
The product of two Haar measures μ on G and ν on H is a Haar measure on G × H (in the symmetric/dual instance).
Русский
Произведение двух мер Хаара μ на G и ν на H является мерой Хаара на G × H (симметричная версия).
LaTeX
$$IsHaarMeasure (μ.prod ν)$$
Lean4
/-- If the neutral element of a group is not isolated, then a Haar measure on this group has
no atoms.
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.
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) noAtoms [IsTopologicalGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G]
[(𝓝[≠] (1 : G)).NeBot] (μ : Measure G) [μ.IsHaarMeasure] : NoAtoms μ := by
cases eq_or_ne (μ 1) 0 with
| inl h => constructor; simpa
| inr h =>
obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩) K_compact.measure_lt_top.ne
