addHaar_real_closedBall' — Mathlib

English

Let μ be a Haar measure on E and hr ≥ 0. Then μ.real(closedBall x r) = r^finrank E · μ.real(closedBall 0 1).

Русский

Пусть μ — мера Хаара на E и hr ≥ 0. Тогда μ.real(closedBall x r) = r^finrank E · μ.real(closedBall 0,1).

LaTeX

$$$\mu_{\mathbb{R}}(\overline{B}(x, r)) = r^{\mathrm{finrank}\,\mathbb{R} E} \cdot \mu_{\mathbb{R}}(\overline{B}(0, 1))$$$

Lean4

theorem addHaar_real_closedBall' (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ.real (closedBall x r) = r ^ finrank ℝ E * μ.real (closedBall 0 1) :=
  by
  simp only [measureReal_def, addHaar_closedBall' μ x hr, ENNReal.toReal_mul, mul_eq_mul_right_iff,
    ENNReal.toReal_ofReal_eq_iff]
  left
  positivity

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