measure_parallelepiped — Mathlib

English

For any x and r ≥ 0, μ.real (closedBall x r) = r^finrank E · μ.real (ball 0 1).

Русский

Для любых x и r ≥ 0 верно: μ.real(closedBall x r) = r^finrank E · μ.real(ball 0 1).

LaTeX

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

Lean4

theorem _root_.AlternatingMap.measure_parallelepiped (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) (v : Fin n → G) :
    ω.measure (parallelepiped v) = ENNReal.ofReal |ω v| :=
  by
  conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]
  simp only [addHaar_parallelepiped, AlternatingMap.measure, coe_nnreal_smul_apply, AlternatingMap.smul_apply,
    Algebra.id.smul_eq_mul, abs_mul, ENNReal.ofReal_mul (abs_nonneg _), ← Real.enorm_eq_ofReal_abs, enorm]

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