Theorem: isLittleO_mul_add_sq (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => a * x + b) =o[atTop] fun x => x ^ 2
Tactic:
apply IsLittleO.add
State after:
case h₁
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => a * x) =o[atTop] fun x => x ^ 2

case h₂
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => b) =o[atTop] fun x => x ^ 2

State before:
case h₁
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => a * x) =o[atTop] fun x => x ^ 2
Tactic:
apply IsLittleO.const_mul_left
State after:
case h₁.h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => x) =o[atTop] fun x => x ^ 2

State before:
case h₁.h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => x) =o[atTop] fun x => x ^ 2
Tactic:
simpa using isLittleO_pow_pow_atTop_of_lt (𝕜 := ℝ) one_lt_two
State after:
no goals

State before:
case h₂
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => b) =o[atTop] fun x => x ^ 2
Tactic:
apply isLittleO_const_of_tendsto_atTop _ <| tendsto_pow_atTop (by linarith)
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ 2 ≠ 0
Tactic:
linarith
State after:
no goals