expGrowthInf_le_expGrowthSup

Mathlib.Analysis.Asymptotics.ExpGrowth

URI: https://scilib.ai/kg/mathlib#ExpGrowth.expGrowthInf_le_expGrowthSup

English

expGrowthInf_le_expGrowthSup: always, the lower growth rate is bounded above by the upper growth rate.

Русский

Всегда нижняя скорость роста меньше или равна верхней скоростью роста.

LaTeX

$$$\\expGrowthInf(u) \\leq \\expGrowthSup(u).$$$

Lean4

theorem expGrowthInf_le_expGrowthSup : expGrowthInf u ≤ expGrowthSup u :=
  liminf_le_limsup

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru