English
There is a canonical measure space on a finite-dimensional inner product space E defined by an orthonormal basis; the volume normalization gives unit parallelepipeds.
Русский
Существует каноническая мера пространства на конечномерном пространстве E, заданная ортонормированным базисом; нормировка объема даёт единый объём параллелепипеда.
LaTeX
$$$\text{measureSpaceOfInnerProductSpace}(E) = \text{volume}$$$
Lean4
/-- If `μ` satisfies `QuotientMeasureEqMeasurePreimage` relative to a both left- and right-
invariant measure `ν` on `G`, then it is a `G` invariant measure on `G ⧸ Γ`. -/
@[to_additive]
theorem smulInvariantMeasure_quotient [IsMulLeftInvariant ν] [hasFun : HasFundamentalDomain Γ.op G ν] :
SMulInvariantMeasure G (G ⧸ Γ) μ where
measure_preimage_smul g A
hA := by
have meas_π : Measurable π := continuous_quotient_mk'.measurable
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
have h𝓕_translate_fundom : IsFundamentalDomain Γ.op (g • 𝓕) ν := h𝓕.smul_of_comm g
erw [h𝓕.projection_respects_measure_apply (μ := μ) (meas_π (measurableSet_preimage (measurable_const_smul g) hA)),
h𝓕_translate_fundom.projection_respects_measure_apply (μ := μ) hA]
change ν ((π ⁻¹' _) ∩ _) = ν ((π ⁻¹' _) ∩ _)
set π_preA := π ⁻¹' A
have : π ⁻¹' ((fun x : G ⧸ Γ => g • x) ⁻¹' A) = (g * ·) ⁻¹' π_preA := by ext1; simp [π_preA]
rw [this]
have : ν ((g * ·) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕) :=
by
trans ν ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
· rw [preimage_inter]
congr 2
simp [Set.preimage]
rw [measure_preimage_mul]
rw [this, ← preimage_smul_inv]; rfl
