prod_addHaar — Mathlib

English

The Haar measure on a product of two real finite-dimensional spaces equals the product of their Haar measures: the product basis yields the product Haar measure.

Русский

Мера Хаара на произведении двух вещественных конечномерных пространств равна произведению их мер Хаара.

LaTeX

$$$(v.prod w).addHaar = v.addHaar.prod w.addHaar$$$

Lean4

theorem prod_addHaar (v : Basis ι ℝ E) (w : Basis ι' ℝ F) : (v.prod w).addHaar = v.addHaar.prod w.addHaar :=
  by
  have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis v
  have : FiniteDimensional ℝ F := FiniteDimensional.of_fintype_basis w
  simp [(v.prod w).addHaar_eq_iff, Basis.prod_parallelepiped, Basis.addHaar_self]

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