English
For a finite-index lattice basis b of L, the volume of the image of a set s under the associated linear isomorphism equals the volume of s divided by covolume(L).
Русский
Для базы L с конечным индексом b объём образа множества s под соответствующим линейным отображением равен объёму s, делённому на коволюм L.
LaTeX
$$$\\operatorname{vol}\\big( (b_{\\mathrm{ofZLatticeBasis}}\\; \\mathbb{R} L)^{\\!\\mathrm{equivFun}}'' s \\big) = \\dfrac{\\operatorname{vol}(s)}{\\operatorname{covolume}(L)}$$$
Lean4
theorem volume_image_eq_volume_div_covolume {ι : Type*} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L]
[IsZLattice ℝ L] (b : Basis ι ℤ L) {s : Set (ι → ℝ)} :
volume ((b.ofZLatticeBasis ℝ L).equivFun '' s) = volume s / ENNReal.ofReal (covolume L) := by
rw [LinearEquiv.image_eq_preimage, Measure.addHaar_preimage_linearEquiv, LinearEquiv.symm_symm,
covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul,
ENNReal.ofReal_inv_of_pos (abs_pos.mpr (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]
