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