English
Under mild nondegeneracy conditions, expGrowthInf (u · v) ≤ expGrowthSup u + expGrowthInf v.
Русский
При мягких условиях невыраженности, expGrowthInf (u · v) ≤ expGrowthSup u + expGrowthInf v.
LaTeX
$$$\text{If suitable nondegeneracy conditions hold } \expGrowthInf(u \cdot v) \le \expGrowthSup(u) + \expGrowthInf(v)$$$
Lean4
/-- See `expGrowthInf_mul_le'` for a version with swapped argument `u` and `v`. -/
theorem expGrowthInf_mul_le (h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤)
(h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥) : expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v :=
by
refine (liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))
rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
