BigO pow lemma

Stream: Is there code for X?

[Moritz Doll]

Hi,
is this lemma somewhere in mathlib? And if not where should it be? I know very little about the asymptotics files.

variable {α : Type*} {l : Filter α}

theorem isBigO_pow_of_le_right {f : α → ℝ} (hf : ∀ x, 1 ≤ f x) {m n : ℕ} (h : n ≤ m) :
    (fun x ↦ (f x) ^ n) =O[l] fun x ↦ (f x) ^ m := by
  apply IsBigO.of_norm_le
  intro x
  specialize hf x
  rw [norm_pow, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans hf)]
  gcongr
  exact hf

Golfs are also highly appreciated

[Yury G. Kudryashov]

You should assume EventuallyLE instead of hf.

[Yury G. Kudryashov]

This lemma is not in Mathlib.

[Yury G. Kudryashov]

When you add it, please add similar lemmas for other inequalities and for IsLittleO (you may need something like "eventually greater than a constant greater than one" here).

[Kenny Lau]

probably can be generalised along the lines of:

import Mathlib

variable {α : Type*} {l : Filter α}

namespace Asymptotics.IsBigO

theorem pow_right {m n : ℕ} (hnm : n ≤ m) {l : Filter ℝ}
    (h : ∀ᶠ x in l, 1 ≤ x) :
    (fun x ↦ x ^ n) =O[l] (fun x ↦ x ^ m) := by
  rw [IsBigO_def]
  refine ⟨1, ?_⟩
  rw [IsBigOWith_def]
  refine h.mono fun x hx ↦ ?_
  simp [abs_eq_self.mpr (by linarith : 0 ≤ x), pow_le_pow_right₀ hx hnm]

end Asymptotics.IsBigO

(and also the two def lemmas are wrongly named, the Is should be lower case?

[Yury G. Kudryashov]

I guess, the _def lemmas are produced by irreducible_def. You can change its logic, then you should add deprecated aliases for all the _def lemmas it used to produce.

[Kenny Lau]

oh i didnt know that, that's quite a handful of irreducible_defs