English
Any regular Haar measure is invariant under inversion in an abelian group.
Русский
Любая регулярная мера Хаара инвариантна по отношению к инверсии в абелевой группе.
LaTeX
$$$\\forall G \\, [\\text{CommGroup } G] \\, [TopologicalSpace G] \\, [IsTopologicalGroup G] \\, [MeasurableSpace G] \\, [BorelSpace G] \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{LocallyCompactSpace } G] \\, [\\text{Regular } μ] \\, IsInvInvariant μ$$
Lean4
/-- Any inner regular Haar measure is invariant under inversion in an abelian group. -/
@[to_additive /-- Any regular additive Haar measure is invariant under negation in an abelian group. -/
]
instance (priority := 100) isInvInvariant_of_innerRegular [LocallyCompactSpace G] [InnerRegular μ] : IsInvInvariant μ :=
by
-- the image measure is a Haar measure. By uniqueness up to multiplication, it is of the form
-- `c μ`. Applying again inversion, one gets the measure `c^2 μ`. But since inversion is an
-- involution, this is also `μ`. Hence, `c^2 = 1`, which implies `c = 1`.
constructor
let c : ℝ≥0∞ := haarScalarFactor μ.inv μ
have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_innerRegular μ.inv μ
have : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ := by
rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
have μeq : μ = c ^ 2 • μ :=
by
rw [map_map continuous_inv.measurable continuous_inv.measurable] at this
simpa only [inv_involutive, Involutive.comp_self, Measure.map_id]
have K : PositiveCompacts G := Classical.arbitrary _
have : c ^ 2 * μ K = 1 ^ 2 * μ K := by
conv_rhs => rw [μeq]
simp
have : c ^ 2 = 1 ^ 2 :=
(ENNReal.mul_left_inj (measure_pos_of_nonempty_interior _ K.interior_nonempty).ne' K.isCompact.measure_lt_top.ne).1
this
have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
rw [hc, this, one_smul]
