English
For nonempty index type, the cardinality ratio converges to volume/ covolume in the inner-product setting.
Русский
При непустом индексе кардинальный соотношение сходится к объему, делённому на коволюм, в случае пространства с внутренним произведением.
LaTeX
$$$\\text{tendsto card le div}'(L) : \\; \\to \\frac{\\operatorname{volume}(X)}{\\operatorname{covolume}(L)}$$$
Lean4
/-- A version of `ZLattice.covolume.tendsto_card_le_div` for the `InnerProductSpace` case;
see the `Naming convention` section in the introduction. -/
theorem tendsto_card_le_div' [Nontrivial E] {X : Set E} {F : E → ℝ} (hX : ∀ ⦃x⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
(h₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * (F x)) (h₂ : IsBounded ({x ∈ X | F x ≤ 1}))
(h₃ : MeasurableSet ({x ∈ X | F x ≤ 1})) (h₄ : volume (frontier ({x ∈ X | F x ≤ 1})) = 0) :
Tendsto (fun c : ℝ ↦ Nat.card ({x ∈ X | F x ≤ c} ∩ L : Set E) / (c : ℝ)) atTop
(𝓝 (volume.real ({x ∈ X | F x ≤ 1}) / covolume L)) :=
by
let b := Module.Free.chooseBasis ℤ L
convert tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
· simp only [measureReal_def]
rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
ENNReal.toReal_ofReal (covolume_pos L volume).le]
· have : Nontrivial L := nontrivial_of_finrank_pos <| (ZLattice.rank ℝ L).symm ▸ finrank_pos
infer_instance
· rwa [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]
· rw [frontier_equivFun, volume_image_eq_volume_div_covolume', h₄, ENNReal.zero_div]
exact NullMeasurableSet.of_null h₄
