Theorem: Asymptotics.IsBigO.add_isLittleO_right (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : g =o[atTop] f
⊢ f =O[atTop] (f + g)
Tactic:
rw [isLittleO_iff] at h
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ f =O[atTop] (f + g)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ f =O[atTop] (f + g)
Tactic:
specialize h (c := 2⁻¹) (by norm_num)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ f =O[atTop] (f + g)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ f =O[atTop] (f + g)
Tactic:
rw [isBigO_iff'']
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖f x‖ ≤ ‖(f + g) x‖

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖f x‖ ≤ ‖(f + g) x‖
Tactic:
refine ⟨2⁻¹, by norm_num, ?_⟩
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∀ᶠ (x : ℝ) in atTop, 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ ∀ᶠ (x : ℝ) in atTop, 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖
Tactic:
filter_upwards [h] with x h
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ 2⁻¹ * ‖f x‖ ≤ ‖(f + g) x‖
Tactic:
simp at h ⊢
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| ≤ |f x + g x|

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| ≤ |f x + g x|
Tactic:
calc _ = |f x| - 2⁻¹ * |f x| := by ring
     _ ≤ |f x| - |g x| := by linarith
     _ ≤ |(|f x| - |g x|)| := le_abs_self _
     _ ≤ _ := by rw [← sub_neg_eq_add, ← abs_neg (g x)] ; exact abs_abs_sub_abs_le (f x) (-g x)
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
⊢ 0 < 2⁻¹
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
⊢ 2⁻¹ > 0
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| = |f x| - 2⁻¹ * |f x|
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ |f x| - 2⁻¹ * |f x| ≤ |f x| - |g x|
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ ||f x| - |g x|| ≤ |f x + g x|
Tactic:
rw [← sub_neg_eq_add, ← abs_neg (g x)]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ ||f x| - |(-g x)|| ≤ |f x - -g x|

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ ||f x| - |(-g x)|| ≤ |f x - -g x|
Tactic:
exact abs_abs_sub_abs_le (f x) (-g x)
State after:
no goals