English
Let a ∈ R with a ≥ 0. Then ⌊a x⌋₊ / x → a as x → ∞.
Русский
Пусть a ∈ R, a ≥ 0. Тогда ⌊a x⌋₊ / x → a при x → ∞.
LaTeX
$$$$\\\\lim_{x \\to \\infty} \\\\frac{\\\\lfloor a x \\\\rfloor_{+}}{x} = a.$$$$
Lean4
theorem tendsto_nat_floor_mul_div_atTop {a : R} (ha : 0 ≤ a) : Tendsto (fun x ↦ (⌊a * x⌋₊ : R) / x) atTop (𝓝 a) :=
by
have A : Tendsto (fun x : R ↦ a - x⁻¹) atTop (𝓝 (a - 0)) := tendsto_const_nhds.sub tendsto_inv_atTop_zero
rw [sub_zero] at A
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul, inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']
have := Nat.lt_floor_add_one (a * x)
linarith
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
rw [div_le_iff₀ (zero_lt_one.trans_le hx)]
simp [Nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))]
