Theorems · Theorem · number theory

ZLattice.covolume.tendsto_card_le_div

∀ {ι : Type u_1} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  {X : Set (ι → ℝ)},
  (∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) →
    ∀ {F : (ι → ℝ) → ℝ},
      (∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) →
        Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1} →
          MeasurableSet {x | x ∈ X ∧ F x ≤ 1} →
            MeasureTheory.volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0 →
              ∀ [Nonempty ι],
                Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop
                  (nhds (MeasureTheory.volume.real {x | x ∈ X ∧ F x ≤ 1} / 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

FintypeDiscreteTopologyIsZLatticeNonempty