expGrowthInf_inf — Mathlib

English

The infimum growth of the pointwise minimum equals the minimum of the infimum growths: expGrowthInf(u ⊓ v) = expGrowthInf(u) ⊓ expGrowthInf(v).

Русский

Падение инфимум роста под точечным минимумом равно минимуму роста: expGrowthInf(u ⊓ v) = expGrowthInf(u) ⊓ expGrowthInf(v).

LaTeX

$$$\expGrowthInf(u \inf v) = \expGrowthInf(u) \inf \expGrowthInf(v)$$$

Lean4

theorem expGrowthInf_inf : expGrowthInf (u ⊓ v) = expGrowthInf u ⊓ expGrowthInf v :=
  by
  rw [expGrowthInf, expGrowthInf, expGrowthInf, ← liminf_min]
  refine liminf_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.inf_apply, log_monotone.map_min]
  exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

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