tendsto_card_div_pow'' — Mathlib

English

Let L be a lattice in a finite-dimensional space; as n grows, the normalized count of lattice points in n^{-1}L within a bounded set converges to the volume of the image of the set under the basis map, divided by covolume.

Русский

Пусть L — решетка в конечномерном пространстве; по мере роста n нормированное число точек решетки внутри масштаба n^{-1}L сходится к отношению объема образа множества при базисном отображении к коволюму.

LaTeX

$$$\\text{Tendsto}\\;\\big( \\frac{\\lvert s \\cap (n^{-1})\\cdot L \\rvert}{n^{\\mathrm{card}\\;\\iota}} \\big)\\to \\frac{\\operatorname{volume}_{\\mathbb{R}}((b.ofZLattice}\\;\\mathbb{R}L)^{\\!\\mathrm{equivFun}}'' s)}{\\operatorname{covolume}(L)}$$$

Lean4

/-- A version of `ZLattice.covolume.tendsto_card_div_pow` for the general case;
see the `Naming convention` section in the introduction. -/
theorem tendsto_card_div_pow'' [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E}
    (hs₁ : IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : volume (frontier ((b.ofZLatticeBasis ℝ).equivFun '' s)) = 0) :
    Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set E) : ℝ) / n ^ card ι) atTop
      (𝓝 (volume.real ((b.ofZLatticeBasis ℝ).equivFun '' s))) :=
  by
  refine Tendsto.congr' ?_ (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
  · filter_upwards [eventually_gt_atTop 0] with n hn
    congr
    refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm
    simp_rw [Set.mem_inter_iff, ← b.ofZLatticeBasis_span ℝ, LinearEquiv.coe_toEquiv, Basis.equivFun_apply,
      Set.mem_image, DFunLike.coe_fn_eq, EmbeddingLike.apply_eq_iff_eq, exists_eq_right, and_congr_right_iff,
      Set.mem_inv_smul_set_iff₀ (mod_cast hn.ne' : (n : ℝ) ≠ 0), ← Finsupp.coe_smul, ← LinearEquiv.map_smul,
      SetLike.mem_coe, Basis.mem_span_iff_repr_mem, Pi.basisFun_repr, implies_true]
  · rw [← NormedSpace.isVonNBounded_iff ℝ] at hs₁ ⊢
    exact Bornology.IsVonNBounded.image hs₁ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hs₂

Похожие утверждения