[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
by_cases h : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
simp [h, IsEquivalent.refl]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x =>
      (Finset.sum (range (natDegree P)) fun i => coeff P i * x ^ i) + coeff P (natDegree P) * x ^ natDegree P) ~[atTop]
    fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
exact
  IsLittleO.add_isEquivalent
    (IsLittleO.sum fun i hi =>
      IsLittleO.const_mul_left
        ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
          isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
        _)
    IsEquivalent.refl
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atTop ↔ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
refine' ⟨fun h => _, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
have : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop := (isEquivalent_atTop_lead P).tendsto_atTop h
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this 
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : 0 < degree P ∧ 0 < leadingCoeff P
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
exact ⟨this.1, this.2.le⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atBot ↔ 0 < degree P ∧ leadingCoeff P ≤ 0
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg, degree_neg, leadingCoeff_neg,
  neg_nonneg]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
⊢ Tendsto (fun x => |eval x P|) atTop atTop
[PROOFSTEP]
cases' le_total 0 P.leadingCoeff with hP hP
[GOAL]
case inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : 0 ≤ leadingCoeff P
⊢ Tendsto (fun x => |eval x P|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)
[GOAL]
case inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : leadingCoeff P ≤ 0
⊢ Tendsto (fun x => |eval x P|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => |eval x P|) ↔ degree P ≤ 0
[PROOFSTEP]
refine'
  ⟨fun h => _, fun h =>
    ⟨|P.coeff 0|,
      eventually_map.mpr
        (eventually_of_forall
          (forall_imp (fun _ => le_of_eq) fun x =>
            congr_arg abs <| _root_.trans (congr_arg (eval x) (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => |eval x P|
⊢ degree P ≤ 0
[PROOFSTEP]
contrapose! h
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : 0 < degree P
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => |eval x P|
[PROOFSTEP]
exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
have := P.isEquivalent_atTop_lead.tendsto_nhds h
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
by_cases hP : P.leadingCoeff = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
simp only [hP, zero_mul, tendsto_const_nhds_iff] at this 
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
refine' ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ degree P ≤ 0
[PROOFSTEP]
simp [leadingCoeff_eq_zero.1 hP]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this 
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : degree P ≤ 0 ∧ leadingCoeff P = c
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
exact this.symm
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c)
[PROOFSTEP]
refine' P.isEquivalent_atTop_lead.symm.tendsto_nhds _
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
[PROOFSTEP]
have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
[PROOFSTEP]
simp only [h.1, this, pow_zero, mul_one]
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => c) atTop (𝓝 c)
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
by_cases hP : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
simp [hP, IsEquivalent.refl]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
by_cases hQ : Q = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : Q = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
simp [hQ, IsEquivalent.refl]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
refine'
  (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
    (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => _))
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
x : 𝕜
hx : 0 < x
⊢ (fun x => leadingCoeff P * x ^ natDegree P / (leadingCoeff Q * x ^ natDegree Q)) x =
    (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) x
[PROOFSTEP]
simp [← div_mul_div_comm, hP, hQ, zpow_sub₀ hx.ne.symm]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
by_cases hP : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
simp [hP, tendsto_const_nhds]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff hP] at hdeg 
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_nhds _
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
[PROOFSTEP]
rw [← mul_zero]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 (?neg✝ * 0))
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ 𝕜
[PROOFSTEP]
refine' (tendsto_zpow_atTop_zero _).const_mul _
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ ↑(natDegree P) - ↑(natDegree Q) < 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ degree P < degree Q
[PROOFSTEP]
refine' ⟨fun h => _, div_tendsto_zero_of_degree_lt P Q⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
⊢ degree P < degree Q
[PROOFSTEP]
by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ 
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : leadingCoeff P = 0 ∨ leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
cases' hPQ with hP0 hQ0
[GOAL]
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : leadingCoeff P = 0
⊢ degree P < degree Q
[PROOFSTEP]
rw [leadingCoeff_eq_zero.1 hP0, degree_zero]
[GOAL]
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : leadingCoeff P = 0
⊢ ⊥ < degree Q
[PROOFSTEP]
exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')
[GOAL]
case pos.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hQ0 : leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
have := (isEquivalent_atTop_div P Q).tendsto_nhds h
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
this : Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
⊢ degree P < degree Q
[PROOFSTEP]
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this 
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
this :
  ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0 ∨
    ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
[PROOFSTEP]
cases' this with h h
[GOAL]
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
exact absurd h.2 hPQ
[GOAL]
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
[PROOFSTEP]
rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h 
[GOAL]
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
h : natDegree P < natDegree Q ∧ 0 = 0
⊢ degree P < degree Q
[PROOFSTEP]
exact degree_lt_degree h.1
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 (leadingCoeff P / leadingCoeff Q))
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_nhds _
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop
    (𝓝 (leadingCoeff P / leadingCoeff Q))
[PROOFSTEP]
rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ ↑(natDegree P) = ↑(natDegree Q)
[PROOFSTEP]
simp [hdeg, natDegree]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree Q) - ↑(natDegree Q))) atTop
    (𝓝 (leadingCoeff P / leadingCoeff Q))
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop
[PROOFSTEP]
have hQ : Q ≠ 0 := fun h => by
  simp only [h, div_zero, leadingCoeff_zero] at hpos 
  exact hpos.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
h : Q = 0
⊢ False
[PROOFSTEP]
simp only [h, div_zero, leadingCoeff_zero] at hpos 
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
h : Q = 0
hpos : 0 < 0
⊢ False
[PROOFSTEP]
exact hpos.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff hQ] at hdeg 
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_atTop _
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
[PROOFSTEP]
apply Tendsto.const_mul_atTop hpos
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
[PROOFSTEP]
apply tendsto_zpow_atTop_atTop
[GOAL]
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ 0 < ↑(natDegree P) - ↑(natDegree Q)
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
[PROOFSTEP]
have hQ : Q ≠ 0 := fun h => by
  simp only [h, div_zero, leadingCoeff_zero] at hneg 
  exact hneg.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
h : Q = 0
⊢ False
[PROOFSTEP]
simp only [h, div_zero, leadingCoeff_zero] at hneg 
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
h : Q = 0
hneg : 0 < 0
⊢ False
[PROOFSTEP]
exact hneg.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff hQ] at hdeg 
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_atBot _
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atBot
[PROOFSTEP]
apply Tendsto.neg_const_mul_atTop hneg
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
[PROOFSTEP]
apply tendsto_zpow_atTop_atTop
[GOAL]
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ 0 < ↑(natDegree P) - ↑(natDegree Q)
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
by_cases h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
h : 0 ≤ leadingCoeff P / leadingCoeff Q
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
h : ¬0 ≤ leadingCoeff P / leadingCoeff Q
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
h : leadingCoeff P / leadingCoeff Q < 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)
[GOAL]
𝕜 : 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
[PROOFSTEP]
by_cases hp : P = 0
[GOAL]
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
[PROOFSTEP]
simpa [hp] using isBigO_zero (fun x => eval x Q) atTop
[GOAL]
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
[PROOFSTEP]
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
cases' le_iff_lt_or_eq.mp h with h h
[GOAL]
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
[PROOFSTEP]
exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_zero_of_degree_lt P Q h)
[GOAL]
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
[PROOFSTEP]
exact isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_leadingCoeff_div_of_degree_eq P Q h)
