addHaar_closedBall_mul_of_pos — Mathlib

English

Let μ be a Haar measure on a finite-dimensional real vector space E. If r > 0 and s ∈ ℝ, then μ(closedBall x (r·s)) = ENNReal.ofReal(r^finrank E) · μ(closedBall 0 s).

Русский

Пусть μ — мера Хаара на конечномерном пространстве E. При r > 0 и любом s ∈ ℝ верно: μ(closedBall x (r·s)) = ENNReal.ofReal(r^finrank E) · μ(closedBall 0 s).

LaTeX

$$$\mu(closedBall(x, r \cdot s)) = ENNReal.ofReal\left(r^{\mathrm{finrank}\,\mathbb{R} E}\right) \cdot \mu(closedBall(0, s))$$$

Lean4

theorem addHaar_closedBall_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
    μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s) :=
  by
  have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
    simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]
  simp only [this, addHaar_smul, abs_of_nonneg hr.le, addHaar_closedBall_center, abs_pow]

Похожие утверждения