English
A generalized form: volume of the image equals volume of the original set divided by ENNReal.ofReal(covolume(L)).
Русский
Обобщённая форма: объём образа равен объёму исходного множества, делённому на ENNReal.ofReal(коволюм(L)).
LaTeX
$$$\\operatorname{vol}\\big( (b_{\\mathrm{ofZLatticeBasis}}\\; L)^{\\!\\mathrm{equivFun}}'' s \\big) = \\dfrac{\\operatorname{vol}(s)}{\\mathrm{ENNReal}.\\mathrm{ofReal}(\\operatorname{covolume}(L))}$$$
Lean4
/-- A more general version of `ZLattice.volume_image_eq_volume_div_covolume`;
see the `Naming conventions` section in the introduction. -/
theorem volume_image_eq_volume_div_covolume' {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice ℝ L]
{ι : Type*} [Fintype ι] (b : Basis ι ℤ L) {s : Set E} (hs : NullMeasurableSet s) :
volume ((b.ofZLatticeBasis ℝ).equivFun '' s) = volume s / ENNReal.ofReal (covolume L) := by
classical
let e : Fin (finrank ℝ E) ≃ ι :=
Fintype.equivOfCardEq (by rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)])
let f := (EuclideanSpace.equiv ι ℝ).symm.trans ((stdOrthonormalBasis ℝ E).reindex e).repr.toContinuousLinearEquiv.symm
have hf : MeasurePreserving f :=
((stdOrthonormalBasis ℝ E).reindex e).measurePreserving_repr_symm.comp
(EuclideanSpace.volume_preserving_measurableEquiv ι).symm
rw [← hf.measure_preimage hs, ← (covolume_comap L volume volume hf), ←
volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap) (b.ofZLatticeComap ℝ L f.toLinearEquiv),
Basis.ofZLatticeBasis_comap, ← f.image_symm_eq_preimage, ← Set.image_comp]
simp
