English
For sequences u, v: ℕ → ℝ≥0∞, the supremum growth of the product is at least the sum of the supremum growth of u and the infimum growth of v:
expGrowthSup(u) + expGrowthInf(v) ≤ expGrowthSup(u·v).
Русский
Для последовательностей u, v: ℕ → ℝ≥0∞ верно, что sup-предел роста произведения не меньше суммы sup-роста u и inf-роста v: expGrowthSup(u) + expGrowthInf(v) ≤ expGrowthSup(u·v).
LaTeX
$$$\expGrowthSup(u) + \expGrowthInf(v) \le \expGrowthSup(u \cdot v)$$$
Lean4
/-- See `le_expGrowthSup_mul'` for a version with swapped argument `u` and `v`. -/
theorem le_expGrowthSup_mul : expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v) :=
by
refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))
rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
