case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
by_cases hp : P = 0
no goals
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
simpa [hp] using isBigO_zero (fun x => eval x Q) atTop
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
have hPQ : ∀ᶠ x : 𝕜 in atTop, eval x Q = 0 → eval x P = 0 :=
  Filter.mem_of_superset (Polynomial.eventually_no_roots Q hq) fun x h h' => absurd h' h
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : degree P < degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : degree P = degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
cases' le_iff_lt_or_eq.mp h with h h
no goals
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : degree P < degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_zero_of_degree_lt P Q h)
no goals
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : degree P = degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
exact isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_leadingCoeff_div_of_degree_eq P Q h)