English
For Haar measure μ and ω an alternating map on a finite-dimensional space, the measure of a parallelepiped equals ENNReal.ofReal(|ω(v)|) for v representing the base directions.
Русский
Для меры Хаара μ и антаорных отображений ω на конечномерном пространстве мера параллелепипеда равна ENNReal.ofReal(|ω(v)|) при базисе v.
LaTeX
$$$\omega.measure(\text{parallelepiped}(v)) = ENNReal.ofReal\left|\omega(v)\right|$$$
Lean4
theorem addHaar_singleton_add_smul_div_singleton_add_smul {r : ℝ} (hr : r ≠ 0) (x y : E) (s t : Set E) :
μ ({ x } + r • s) / μ ({ y } + r • t) = μ s / μ t :=
calc
μ ({ x } + r • s) / μ ({ y } + r • t) =
ENNReal.ofReal (|r| ^ finrank ℝ E) * μ s * (ENNReal.ofReal (|r| ^ finrank ℝ E) * μ t)⁻¹ :=
by simp only [div_eq_mul_inv, addHaar_smul, image_add_left, measure_preimage_add, abs_pow, singleton_add]
_ = ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ * (μ s * (μ t)⁻¹) :=
by
rw [ENNReal.mul_inv]
· ring
· simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne, true_or]
· simp only [ENNReal.ofReal_ne_top, true_or, Ne, not_false_iff]
_ = μ s / μ t := by
rw [ENNReal.mul_inv_cancel, one_mul, div_eq_mul_inv]
· simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne]
· simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]
