English
Let u, v: ℕ → ℝ≥0∞ be sequences. Then the supremum growth of the product is bounded above by the sum of the supremum growths: expGrowthSup(u·v) ≤ expGrowthSup(u) + expGrowthSup(v).
Русский
Пусть u, v: ℕ → ℝ≥0∞ — последовательности. Тогда sup-рост произведения ограничен сверху суммой sup-ростов: expGrowthSup(u·v) ≤ expGrowthSup(u) + expGrowthSup(v).
LaTeX
$$$\expGrowthSup(u \cdot v) \le \expGrowthSup(u) + \expGrowthSup(v)$$$
Lean4
theorem expGrowthSup_mul_le (h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤)
(h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥) : expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v :=
by
refine (limsup_add_le h h').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']
