English
For any monotone u and natural m ≠ 0, the infimum of u(mn) equals m times the infimum of u: linearGrowthInf (n ↦ u(m n)) = m · linearGrowthInf u.
Русский
Пусть u монотонна; для любого натурального m ≠ 0 нижний рост композиции с умножением аргумента равен m · нижнему росту u: linearGrowthInf(u(m n)) = m · linearGrowthInf(u).
LaTeX
$$$\operatorname{linearGrowthInf}(u \circ (\cdot m)) = m \cdot \operatorname{linearGrowthInf}(u)$$$
Lean4
theorem _root_.Monotone.linearGrowthInf_comp_mul {m : ℕ} (h : Monotone u) (hm : m ≠ 0) :
linearGrowthInf (fun n ↦ u (m * n)) = m * linearGrowthInf 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.linearGrowthInf_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)
