Theorems · Theorem · number theory

ZLattice.covolume.tendsto_card_div_pow

∀ {ι : Type u_1} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)},
  Bornology.IsBounded s →
    MeasurableSet s →
      MeasureTheory.volume (frontier s) = 0 →
        Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop
          (nhds (MeasureTheory.volume.real s / ZLattice.covolume L MeasureTheory.volume))

Defined in

Mathlib.Algebra.Module.ZLattice.Covolume

Cited by

0 results in Mathlib

Foundations

Depth 263 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDiscreteTopologyIsZLattice