English
The canonical Lebesgue volume on a finite-dimensional real vector space is a Haar measure.
Русский
Каноническая мера Лебега на конечномерном вещественном пространстве является мерой Хаара.
LaTeX
$$$IsAddHaarMeasure(volume)$$$
Lean4
/-- If `μ` on `G ⧸ Γ` satisfies `QuotientMeasureEqMeasurePreimage` relative to a both left- and
right-invariant measure on `G` and `Γ` is a normal subgroup, then `μ` is a left-invariant
measure. -/
@[to_additive /-- If `μ` on `G ⧸ Γ` satisfies `AddQuotientMeasureEqMeasurePreimage` relative to a
both left- and right-invariant measure on `G` and `Γ` is a normal subgroup, then `μ` is a
left-invariant measure. -/
]
theorem mulInvariantMeasure_quotient [hasFun : HasFundamentalDomain Γ.op G ν] [QuotientMeasureEqMeasurePreimage ν μ] :
μ.IsMulLeftInvariant where
map_mul_left_eq_self
x := by
ext A hA
obtain ⟨x₁, h⟩ := @Quotient.exists_rep _ (QuotientGroup.leftRel Γ) x
convert measure_preimage_smul μ x₁ A using 1
· rw [← h, Measure.map_apply (measurable_const_mul _) hA]
simp [← MulAction.Quotient.coe_smul_out, ← Quotient.mk''_eq_mk]
exact smulInvariantMeasure_quotient ν
