English
For a ≥ 0, the ratio ⌈a x⌉₊ / x tends to a as x → ∞.
Русский
Пусть a ≥ 0. Тогда ⌈a x⌉₊ / x → a при x → ∞.
LaTeX
$$$$\\\\lim_{x \\to \\infty} \\\\frac{\\\\lceil a x \\\\rceil_{+}}{x} = a.$$$$
Lean4
theorem tendsto_nat_ceil_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.add tendsto_inv_atTop_zero
rw [add_zero] at A
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
rw [le_div_iff₀ (zero_lt_one.trans_le hx)]
exact Nat.le_ceil _
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
simp [div_le_iff₀ (zero_lt_one.trans_le hx), inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne',
(Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]
