English
A more general version: for L1 ≤ L2 inside an ℝ-space lattice, covolume ratio equals the relative index of the associated AddSubgroups.
Русский
Более общая версия: для L1 ≤ L2 внутри надпространства решёт, отношение коволюмов равно относительному индексу соответствующих подгрупп.
LaTeX
$$$\\dfrac{\\operatorname{covolume}(L_1,\\mu)}{\\operatorname{covolume}(L_2,\\mu)} = \\operatorname{relIndex}\\big(L_1^{\\,+}, L_2^{\\,+}\\big)$$$
Lean4
/-- A more general version of `covolume_div_covolume_eq_relIndex`;
see the `Naming conventions` section in the introduction.
-/
theorem covolume_div_covolume_eq_relIndex' {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L₁ L₂ : Submodule ℤ E) [DiscreteTopology L₁]
[IsZLattice ℝ L₁] [DiscreteTopology L₂] [IsZLattice ℝ L₂] (h : L₁ ≤ L₂) :
covolume L₁ / covolume L₂ = L₁.toAddSubgroup.relIndex L₂.toAddSubgroup :=
by
let f := (EuclideanSpace.equiv _ ℝ).symm.trans (stdOrthonormalBasis ℝ E).repr.toContinuousLinearEquiv.symm
have hf : MeasurePreserving f :=
(stdOrthonormalBasis ℝ E).measurePreserving_repr_symm.comp (EuclideanSpace.volume_preserving_measurableEquiv _).symm
rw [← covolume_comap L₁ volume volume hf, ← covolume_comap L₂ volume volume hf,
covolume_div_covolume_eq_relIndex _ _ (fun _ h' ↦ h h'), ZLattice.comap_toAddSubgroup, ZLattice.comap_toAddSubgroup,
Nat.cast_inj, LinearEquiv.toAddMonoidHom_commutes, AddSubgroup.comap_equiv_eq_map_symm',
AddSubgroup.comap_equiv_eq_map_symm', AddSubgroup.relIndex_map_map_of_injective _ _ f.symm.injective]
