English
The limit as n → ∞ of card(s ∩ n⁻¹•L) / n^{card ι} equals the volume of s, under standard regularity assumptions.
Русский
Предел при n → ∞ для отношения между количеством точек в s ∩ n⁻¹•L и степенью n равно объёму множества s, при разумных условиях.
LaTeX
$$$$ \lim_{n\to\infty} \frac{\mathrm{card}\bigl(s \cap (n^{-1})\cdot L\bigr)}{n^{|\iota|}} = \mathrm{volume.real}(s) $$$$
Lean4
/-- Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume. Then the limit
as `n → ∞` of `card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι` tends to the volume of `s`. This is a
special case of `tendsto_card_div_pow` with `F = 1`. -/
theorem _root_.tendsto_card_div_pow_atTop_volume (hs₁ : IsBounded s) (hs₂ : MeasurableSet s)
(hs₃ : volume (frontier s) = 0) :
Tendsto (fun n : ℕ ↦ (Nat.card ↑(s ∩ (n : ℝ)⁻¹ • L) : ℝ) / n ^ card ι) atTop (𝓝 (volume.real s)) :=
by
convert tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃
· rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]
· rw [setIntegral_const, smul_eq_mul, mul_one]
