English
Let μ, μ′ be left-invariant measures on G with Haar property; then μ′ = haarScalarFactor μ′ μ · μ.
Русский
Пусть μ, μ′ — лево-инвариантные меры на G; тогда μ′ = haarScalarFactor μ′ μ · μ.
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsFiniteMeasureOnCompacts } μ'] \\, [\\text{IsMulLeftInvariant } μ'] \\, μ' = haarScalarFactor μ' μ · μ$$
Lean4
/-- Any 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_regular [LocallyCompactSpace G] [Regular μ] : 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_regular μ.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]
