sqrt

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.sqrt

← MathLib Explorer

English

If f = o_l g, then sqrt f = o_l sqrt g.

Русский

Если f = o_l g, тогда sqrt f = o_l sqrt g.

LaTeX

$$$$ \sqrt{f} = o_l (\sqrt{g}) $$$$

Lean4

protected theorem sqrt (hfg : f =o[l] g) (hg : 0 ≤ᶠ[l] g) : (fun x ↦ √(f x)) =o[l] (fun x ↦ √(g x)) := by
  simpa [Real.sqrt_eq_rpow] using hfg.rpow one_half_pos hg

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

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

Разделы

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

Аффилиация

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