tendsto_norm_atTop_iff

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.tendsto_norm_atTop_iff

← MathLib Explorer

English

If f' =Θ[l] g' and f' =Θ[l'] g', then f' =Θ[max(l,l')] g'.

Русский

Если f' =Θ[l] g' и f' =Θ[l'] g', то f' =Θ[max(l,l')] g'.

LaTeX

$$$ (f' =Θ[l] g') \land (f' =Θ[l'] g') \Rightarrow f' =Θ[l \lor l'] g'. $$$

Lean4

theorem tendsto_norm_atTop_iff (h : f' =Θ[l] g') : Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop := by
  simp only [Function.comp_def, ← isLittleO_const_left_of_ne (one_ne_zero' ℝ), h.isLittleO_congr_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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