English
In InnerProductSpace setting, for a lattice L with a finite index basis, the analogous limit holds with finrank replacing card ι.
Русский
В пространстве сInnerProduct, для решетки L и базиса конечного индекса, аналогичное ограничение выполняется с finrank вместо card ι.
LaTeX
$$$\\text{tendsto card div pow}'(L,b) \quad\\text{gives } \\frac{\\mathrm{vol}(s)}{\\operatorname{covolume}(L)}$$$
Lean4
/-- A version of `ZLattice.covolume.tendsto_card_div_pow` for the `InnerProductSpace` case;
see the `Naming convention` section in the introduction. -/
theorem tendsto_card_div_pow' {s : Set E} (hs₁ : IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) :
Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set E) : ℝ) / n ^ finrank ℝ E) atTop
(𝓝 (volume.real s / covolume L)) :=
by
let b := Module.Free.chooseBasis ℤ L
convert tendsto_card_div_pow'' b hs₁ hs₂ ?_
· rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]
· simp only [measureReal_def]
rw [volume_image_eq_volume_div_covolume' L b hs₂.nullMeasurableSet, ENNReal.toReal_div,
ENNReal.toReal_ofReal (covolume_pos L volume).le]
· rw [frontier_equivFun, volume_image_eq_volume_div_covolume', hs₃, ENNReal.zero_div]
exact NullMeasurableSet.of_null hs₃
