English
An invariant σ-finite left-invariant measure μ is absolutely continuous with respect to a Haar measure ν on a second countable group.
Русский
Неизменяемая σ-сконечная левая мера μ относительна к мере Хаара ν на второй счетной группе.
LaTeX
$$$\\forall G, \\mu, \\nu : \\mathrm{Measure}(G), [\\text{IsHaarMeasure } ν], [\\text{IsMulLeftInvariant } μ], [\\text{SigmaFinite } μ] \\, \\mu \\ll \\nu$$
Lean4
/-- An invariant σ-finite measure is absolutely continuous with respect to a Haar measure in a
second countable group. -/
@[to_additive /-- An invariant measure is absolutely continuous with respect to an additive Haar measure. -/
]
theorem absolutelyContinuous_isHaarMeasure [LocallyCompactSpace G] [SecondCountableTopology G] (μ ν : Measure G)
[SigmaFinite μ] [IsMulLeftInvariant μ] [IsHaarMeasure ν] : μ ≪ ν :=
by
have K : PositiveCompacts G := Classical.arbitrary _
have h : haarMeasure K = (haarScalarFactor (haarMeasure K) ν : ℝ≥0∞) • ν :=
isMulLeftInvariant_eq_smul (haarMeasure K) ν
rw [haarMeasure_unique μ K, h, smul_smul]
exact smul_absolutelyContinuous
