mul_atTop_rpow_of_isBigO_rpow — Mathlib

English

If f = O_atTop t^a and g = O_atTop t^b, and a + b ≤ c, then f · g = O_atTop t^c.

Русский

Если f = O_atTop t^a и g = O_atTop t^b и a + b ≤ c, то f·g = O_atTop t^c.

LaTeX

$$$$ (f g) = O_{\mathrm{atTop}} \bigl(t \mapsto t^c\bigr) $$$$

Lean4

theorem mul_atTop_rpow_of_isBigO_rpow {f g : ℝ → E} (hf : f =O[atTop] fun t ↦ (t : ℝ) ^ a)
    (hg : g =O[atTop] fun t ↦ (t : ℝ) ^ b) (h : a + b ≤ c) : (f * g) =O[atTop] fun t ↦ (t : ℝ) ^ c :=
  by
  refine (hf.mul hg).trans (Eventually.isBigO ?_)
  filter_upwards [eventually_ge_atTop 1] with t ht
  rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg (zero_le_one.trans ht) (a + b))]
  exact Real.rpow_le_rpow_of_exponent_le ht h

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