addHaar_closedBall — Mathlib

English

Let μ be Haar on E. For any x, r ≥ 0, we have μ(closedBall x (r)) = ENNReal.ofReal(r^finrank E) · μ(closedBall 0 1).

Русский

Пусть μ — мера Хаара на E. Для любого x и r ≥ 0 выполняется: μ(closedBall x (r)) = ENNReal.ofReal(r^finrank E) · μ(closedBall 0 1).

LaTeX

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

Lean4

theorem addHaar_closedBall (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) := by
  rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unitBall]

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