le_expGrowthInf_mul — Mathlib

English

expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u · v).

Русский

expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u · v).

LaTeX

$$$\expGrowthInf(u) + \expGrowthInf(v) \le \expGrowthInf(u \cdot v)$$$

Lean4

theorem le_expGrowthInf_mul : expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v) :=
  by
  refine le_liminf_add.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]

Похожие утверждения