English
Under standard normed-module assumptions, Tendsto of floor-based smul coincides with Tendsto of the original smul in the target limit.
Русский
При обычных предположениях нормированных модулей предел для floor-умножения совпадает с пределом исходного умножения.
LaTeX
$$$\text{Tendsto}(x \mapsto x \cdot g(\lfloor x \rfloor_+)) (\text{atTop}) (\nhds t) \;\Rightarrow\; \text{Tendsto}(n \mapsto n \cdot g(n)) (\text{atTop}) (\nhds t)$$$
Lean4
theorem apply_mul_add_le (k n r) : u (k * n + r) ≤ k * u n + u r := by
induction k with
| zero => simp only [Nat.cast_zero, zero_mul, zero_add]; rfl
| succ k IH =>
calc
u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
_ ≤ u n + u (k * n + r) := (h _ _)
_ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
_ = (k + 1 : ℕ) * u n + u r := by simp; ring
