-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) :
    deriv (fun z => z ^ p * (1 + ε z)) ~[atTop] fun z => p * z ^ (p-1) := calc
  deriv (fun z => z ^ p * (1 + ε z))
    =ᶠ[atTop] fun z => p * z ^ (p-1) * (1 + ε z) - z ^ (p-1) / (log z ^ 2) :=
        eventually_deriv_rpow_p_mul_one_add_smoothingFn p
  _ ~[atTop] fun z => p * z ^ (p-1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / log z ^ 2) ~[atTop] fun z => p * z ^ (p - 1)

Tactic:
refine IsEquivalent.add_isLittleO ?one ?two

Result:
case one
p : ℝ
hp : p ≠ 0
⊢ (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1)

case two
p : ℝ
hp : p ≠ 0
⊢ (fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => p * z ^ (p - 1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => p * z ^ (p - 1)

Tactic:
calc
(fun z => -(z ^ (p-1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p-1) / 1 := by
  simp_rw [isLittleO_neg_left, div_eq_mul_inv]
  refine IsBigO.mul_isLittleO (isBigO_refl _ _)
    (IsLittleO.inv_rev ?_ (by simp))
  rw [isLittleO_const_left]
  refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
  exact Tendsto.comp (g := fun z => z ^ 2)
    (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
_ = fun z => z ^ (p-1) := by ext; simp
_ =Θ[atTop] fun z => p * z ^ (p-1) := by
  exact IsTheta.const_mul_right hp <| isTheta_refl _ _

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => z ^ (p - 1)) =Θ[atTop] fun z => p * z ^ (p - 1)

Tactic:
exact IsTheta.const_mul_right hp <| isTheta_refl _ _

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1)

Tactic:
calc
(fun z => p * z ^ (p-1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p-1) * 1 :=
IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
_ = fun z => p * z ^ (p-1) := by ext; ring

Result:
no goals

Proof state:
case one
p : ℝ
hp : p ≠ 0
⊢ (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1)

case two
p : ℝ
hp : p ≠ 0
⊢ (fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => p * z ^ (p - 1)

Tactic:
case one => calc
  (fun z => p * z ^ (p-1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p-1) * 1 :=
        IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
  _ = fun z => p * z ^ (p-1) := by ext; ring

Result:
case two
p : ℝ
hp : p ≠ 0
⊢ (fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => p * z ^ (p - 1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => p * z ^ (p - 1) * 1) = fun z => p * z ^ (p - 1)

Tactic:
ext

Result:
case h
p : ℝ
hp : p ≠ 0
x✝ : ℝ
⊢ p * x✝ ^ (p - 1) * 1 = p * x✝ ^ (p - 1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => z ^ (p - 1) / 1) = fun z => z ^ (p - 1)

Tactic:
ext

Result:
case h
p : ℝ
hp : p ≠ 0
x✝ : ℝ
⊢ x✝ ^ (p - 1) / 1 = x✝ ^ (p - 1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, 1 = 0 → log x ^ 2 = 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ 1 = 0 ∨ Tendsto (Norm.norm ∘ fun x => log x ^ 2) atTop atTop

Tactic:
refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Result:
p : ℝ
hp : p ≠ 0
⊢ Tendsto (fun x => log x ^ 2) atTop atTop

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun x => x ^ (p - 1) * (log x ^ 2)⁻¹) =o[atTop] fun z => z ^ (p - 1) * 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _)
  (IsLittleO.inv_rev ?_ (by simp))

Result:
p : ℝ
hp : p ≠ 0
⊢ (fun z => 1) =o[atTop] fun x => log x ^ 2

Proof state:
p : ℝ
hp : p ≠ 0
⊢ Tendsto (fun x => log x ^ 2) atTop atTop

Tactic:
exact Tendsto.comp (g := fun z => z ^ 2)
  (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1

Tactic:
simp_rw [isLittleO_neg_left, div_eq_mul_inv]

Result:
p : ℝ
hp : p ≠ 0
⊢ (fun x => x ^ (p - 1) * (log x ^ 2)⁻¹) =o[atTop] fun z => z ^ (p - 1) * 1⁻¹

Proof state:
case h
p : ℝ
hp : p ≠ 0
x✝ : ℝ
⊢ x✝ ^ (p - 1) / 1 = x✝ ^ (p - 1)

Tactic:
simp

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun z => 1) =o[atTop] fun x => log x ^ 2

Tactic:
rw [isLittleO_const_left]

Result:
p : ℝ
hp : p ≠ 0
⊢ 1 = 0 ∨ Tendsto (Norm.norm ∘ fun x => log x ^ 2) atTop atTop

Proof state:
case h
p : ℝ
hp : p ≠ 0
x✝ : ℝ
⊢ p * x✝ ^ (p - 1) * 1 = p * x✝ ^ (p - 1)

Tactic:
ring

Result:
no goals

Proof state:
case two
p : ℝ
hp : p ≠ 0
⊢ (fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => p * z ^ (p - 1)

Tactic:
case two => calc
  (fun z => -(z ^ (p-1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p-1) / 1 := by
              simp_rw [isLittleO_neg_left, div_eq_mul_inv]
              refine IsBigO.mul_isLittleO (isBigO_refl _ _)
                (IsLittleO.inv_rev ?_ (by simp))
              rw [isLittleO_const_left]
              refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
              exact Tendsto.comp (g := fun z => z ^ 2)
                (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
  _ = fun z => z ^ (p-1) := by ext; simp
  _ =Θ[atTop] fun z => p * z ^ (p-1) := by
              exact IsTheta.const_mul_right hp <| isTheta_refl _ _

Result:
no goals