English
Let u, v be functions from natural numbers to extended nonnegative reals. If the pair (expGrowthInf u, expGrowthSup v) is not degenerate in both directions (precisely, expGrowthInf u ≠ ⊥ or expGrowthSup v ≠ ⊤, and expGrowthInf u ≠ ⊤ or expGrowthSup v ≠ ⊥), then the infimum exponential growth of the pointwise product is bounded above by the sum of the infimum growth of u and the supremum growth of v:
expGrowthInf(u·v) ≤ expGrowthInf(u) + expGrowthSup(v).
Here (u·v)(n) = u(n)·v(n).
Русский
Пусть u, v: ℕ → ℝ≥0∞ — функции. При выполнении условий невырождения (expGrowthInf u ≠ ⊥ или expGrowthSup v ≠ ⊤, и expGrowthInf u ≠ ⊤ или expGrowthSup v ≠ ⊥) выполняется неравенство:
expGrowthInf(u·v) ≤ expGrowthInf(u) + expGrowthSup(v), где (u·v)(n) = u(n)·v(n).
LaTeX
$$$\Big(\expGrowthInf(u) \neq \bot \lor \expGrowthSup(v) \neq \top\Big) \land \Big(\expGrowthInf(u) \neq \top \lor \expGrowthSup(v) \neq \bot\Big) \Rightarrow \expGrowthInf(u \cdot v) \le \expGrowthInf(u) + \expGrowthSup(v)$$$
Lean4
/-- See `expGrowthInf_mul_le` for a version with swapped argument `u` and `v`. -/
theorem expGrowthInf_mul_le' (h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤)
(h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥) : expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v :=
by
rw [mul_comm, add_comm]
exact expGrowthInf_mul_le h'.symm h.symm
