English
The Haar measure of a ball is invariant under translations in a Haar group: μ(ball(x,r)) = μ(ball(0,r)).
Русский
Гааровa мера шара инвариантна относительно переноса по группе: μ(ball(x,r)) = μ(ball(0,r)).
LaTeX
$$\\mu(\\mathsf{ball}(x,r)) = \\mu(\\mathsf{ball}(0,r))$$
Lean4
/-- Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`. -/
@[simp]
theorem addHaar_smul (r : ℝ) (s : Set E) : μ (r • s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * μ s :=
by
rcases ne_or_eq r 0 with (h | rfl)
· rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
rcases eq_empty_or_nonempty s with (rfl | hs)
· simp only [measure_empty, mul_zero, smul_set_empty]
rw [zero_smul_set hs, ← singleton_zero]
by_cases h : finrank ℝ E = 0
· haveI : Subsingleton E := finrank_zero_iff.1 h
simp only [h, one_mul, ENNReal.ofReal_one, abs_one, Subsingleton.eq_univ_of_nonempty hs, pow_zero,
Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))]
· haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)
simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne, not_false_iff, zero_pow, measure_singleton]
