mul_atTop_rpow_natCast_of_isBigO_rpow

English

If hf: f = O_atTop n^a and hg: g = O_atTop n^b for ℕ → E, and a + b ≤ c, then (f · g) = O_atTop n^c.

Русский

Если hf: f = O_atTop n^a и hg: g = O_atTop n^b, и a + b ≤ c, то f·g = O_atTop n^c.

LaTeX

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

Lean4

theorem mul_atTop_rpow_natCast_of_isBigO_rpow {f g : ℕ → E} (hf : f =O[atTop] fun n ↦ (n : ℝ) ^ a)
    (hg : g =O[atTop] fun n ↦ (n : ℝ) ^ b) (h : a + b ≤ c) : (f * g) =O[atTop] fun n ↦ (n : ℝ) ^ c :=
  by
  refine (hf.mul hg).trans (Eventually.isBigO ?_)
  filter_upwards [eventually_ge_atTop 1] with t ht
  replace ht : 1 ≤ (t : ℝ) := Nat.one_le_cast.mpr 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

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