case a
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r
apply IsBigOWith.of_bound
case h
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : OfNat.ofNat 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
case a
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
filter_upwards [hg, h.bound]with x hgx hx
no goals
case h
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : OfNat.ofNat 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
calc
  |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
  _ ≤ (c * |g x|) ^ r := (rpow_le_rpow (abs_nonneg _) hx hr)
  _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
no goals
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : OfNat.ofNat 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (c * abs (g x)) ^ r = c ^ r * abs (g x ^ r)
rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]