English
A real-argument version of the volume limit: the limit for Vol(s) is achieved by a similar summation with real arguments.
Русский
Версия для вещественного аргумента: предел объёма достигается аналогичной суммой с вещественными аргументами.
LaTeX
$$$$ \lim_{x\to\infty} \frac{\#(s \cap x^{-1} \cdot L)}{x^{|\iota|}} = \mathrm{volume.real}(s) $$$$
Lean4
/-- A version of `tendsto_card_div_pow_atTop_volume` for a real variable. -/
theorem _root_.tendsto_card_div_pow_atTop_volume' (hs₁ : IsBounded s) (hs₂ : MeasurableSet s)
(hs₃ : volume (frontier s) = 0) (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) :
Tendsto (fun x : ℝ ↦ (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι) atTop (𝓝 (volume.real s)) :=
by
rw [show volume.real s = volume.real s * 1 ^ card ι by ring]
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le' ?_ ?_ (tendsto_card_div_pow₃ s hs₁ hs₄) (tendsto_card_div_pow₄ s hs₁ hs₄)
· refine Tendsto.congr' (tendsto_card_div_pow₅ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))
· exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_floor_atTop
· exact tendsto_nat_floor_div_atTop
· refine Tendsto.congr' (tendsto_card_div_pow₆ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))
· exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_ceil_atTop
· exact tendsto_nat_ceil_div_atTop
