English
A continuous surjective monoid homomorphism between topological groups with compact codomain preserves Haar measure, provided the total masses agree.
Русский
Пусть моноид-гомоморфизм между топологическими группами непрерывен и сюръективен, кодом является компактная группа; тогда мера сохраняется, если суммарные массы совпадают.
LaTeX
$$$\\forall H \\; [Group H] \\; [TopologicalSpace H] \\; [IsTopologicalGroup H] \\; [CompactSpace H] \\; [MeasurableSpace H] \\; [BorelSpace H] \\\\ (μ : \\mathrm{Measure}(G)) \\; [IsHaarMeasure μ] \\; (ν : \\mathrm{Measure}(H)) [IsHaarMeasure ν] \\\\ (f : G \\to^* H) \\, (hcont : \\text{Continuous } f) \\\\ (huniv : μ(\\mathrm{univ}) = ν(\\mathrm{univ})) \\\\Rightarrow \\text{MeasurePreserving } f \, μ \, ν$$
Lean4
/-- A continuous surjective monoid homomorphism of topological groups with compact codomain
is measure preserving, provided that the Haar measures on the domain and on the codomain
have the same total mass.
-/
@[to_additive /-- A continuous surjective additive monoid homomorphism of topological groups with compact
codomain is measure preserving, provided that the Haar measures on the domain and on the codomain
have the same total mass. -/
]
theorem _root_.MonoidHom.measurePreserving {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
[CompactSpace H] [MeasurableSpace H] [BorelSpace H] {μ : Measure G} [IsHaarMeasure μ] {ν : Measure H}
[IsHaarMeasure ν] {f : G →* H} (hcont : Continuous f) (hsurj : Surjective f) (huniv : μ univ = ν univ) :
MeasurePreserving f μ ν where
measurable := hcont.measurable
map_eq := by
have : IsFiniteMeasure μ := ⟨by rw [huniv]; apply measure_lt_top⟩
have : (μ.map f).IsHaarMeasure := isHaarMeasure_map_of_isFiniteMeasure μ f hcont hsurj
set C : ℝ≥0 := haarScalarFactor (μ.map f) ν
have hC : μ.map f = C • ν := isMulLeftInvariant_eq_smul_of_innerRegular _ _
suffices C = 1 by rwa [this, one_smul] at hC
have : C * ν univ = 1 * ν univ := by
rw [one_mul, ← smul_eq_mul, ← ENNReal.smul_def, ← smul_apply, ← hC, map_apply hcont.measurable .univ,
preimage_univ, huniv]
rwa [ENNReal.mul_left_inj (NeZero.ne _) (measure_ne_top _ _), ENNReal.coe_eq_one] at this
