English
For any monotone u and m ≠ 0, the supremum of u(mn) equals m times the supremum of u: linearGrowthSup (n ↦ u(m n)) = m · linearGrowthSup u.
Русский
Пусть u монотонна; для любого m ≠ 0 верхний рост (u(mn)) равен m · верхнему росту u: linearGrowthSup(u(mn)) = m · linearGrowthSup(u).
LaTeX
$$$\operatorname{linearGrowthSup}(n \mapsto u(mn)) = m \cdot \operatorname{linearGrowthSup}(u)$$$
Lean4
theorem _root_.Monotone.linearGrowthSup_comp_mul {m : ℕ} (h : Monotone u) (hm : m ≠ 0) :
linearGrowthSup (fun n ↦ u (m * n)) = m * linearGrowthSup u :=
by
have : Tendsto (fun n : ℕ ↦ ((m * n : ℕ) : EReal) / n) atTop (𝓝 m) :=
by
refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)
rw [mul_comm, natCast_mul x m, ← mul_div]
exact mul_div_cancel (natCast_ne_bot x) (natCast_ne_top x) (Nat.cast_ne_zero.2 hx.ne.symm)
exact h.linearGrowthSup_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)
