English
For a lattice L and a finite basis b, the volume of the image of a set s under the basis map equals the original volume divided by covolume(L).
Русский
Для решетки L и базиса b, объем образа множества s под отображением базиса равен объему s, делённому на коволюм L.
LaTeX
$$$\\operatorname{vol}\\big( (b.ofZLatticeBasis \\; \\mathbb{R} L)^{\\!\\mathrm{equivFun}}'' s \\big) = \\dfrac{\\operatorname{vol}(s)}{\\operatorname{covolume}(L)}$$$
Lean4
theorem tendsto_card_div_pow (b : Basis ι ℤ L) {s : Set (ι → ℝ)} (hs₁ : IsBounded s) (hs₂ : MeasurableSet s)
(hs₃ : volume (frontier s) = 0) :
Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set (ι → ℝ)) : ℝ) / n ^ card ι) atTop
(𝓝 (volume.real s / covolume L)) :=
by
classical
convert tendsto_card_div_pow'' b hs₁ hs₂ ?_
· simp only [measureReal_def]
rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div, ENNReal.toReal_ofReal (covolume_pos L volume).le]
· rw [frontier_equivFun, volume_image_eq_volume_div_covolume, hs₃, ENNReal.zero_div]
