-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
    GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Proof state:
case h
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log x

Tactic:
exact log_nonneg hx

Result:
no goals

Proof state:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Tactic:
refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_

Result:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun z => z⁻¹ / log z ^ 2

Proof state:
p : ℝ
⊢ GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Tactic:
cases eq_or_ne p 0 with
| inl hp => have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖)
      =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by
    filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
    have : 0 ≤ x⁻¹ / (log x ^ 2) := by
      have hlog : 0 < log x := Real.log_pos hx_pos
      positivity
    simp only [neg_div, norm_neg, hp, Real.rpow_zero,
      one_mul, differentiableAt_const, hx, Real.norm_of_nonneg this]
  refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_
  refine GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
    (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
  filter_upwards [eventually_ge_atTop 1] with x hx
  exact log_nonneg hx
| inr hp => refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1))
    (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_
  filter_upwards [eventually_gt_atTop 0] with _ _
  positivity

Result:
no goals

Proof state:
case inr
p : ℝ
hp : p ≠ 0
⊢ GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Tactic:
refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1))
  (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_

Result:
case inr
p : ℝ
hp : p ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Proof state:
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
⊢ 0 ≤ x⁻¹ / log x ^ 2

Tactic:
have hlog : 0 < log x := Real.log_pos hx_pos

Result:
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
hlog : 0 < log x
⊢ 0 ≤ x⁻¹ / log x ^ 2

Proof state:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ log x

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Result:
case h
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log x

Proof state:
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
hlog : 0 < log x
⊢ 0 ≤ x⁻¹ / log x ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case inl
p : ℝ
hp : p = 0
⊢ GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Tactic:
have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖)
    =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by
  filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
  have : 0 ≤ x⁻¹ / (log x ^ 2) := by
    have hlog : 0 < log x := Real.log_pos hx_pos
    positivity
  simp only [neg_div, norm_neg, hp, Real.rpow_zero,
    one_mul, differentiableAt_const, hx, Real.norm_of_nonneg this]

Result:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Proof state:
p : ℝ
hp : p = 0
⊢ (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2

Tactic:
filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos

Result:
case h
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
⊢ ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ = x⁻¹ / log x ^ 2

Proof state:
case h
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
this : 0 ≤ x⁻¹ / log x ^ 2
⊢ ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ = x⁻¹ / log x ^ 2

Tactic:
simp only [neg_div, norm_neg, hp, Real.rpow_zero,
  one_mul, differentiableAt_const, hx, Real.norm_of_nonneg this]

Result:
no goals

Proof state:
case h
p : ℝ
hp : p ≠ 0
a✝¹ : ℝ
a✝ : 0 < a✝¹
⊢ 0 ≤ ‖deriv (fun z => z ^ p * (1 + ε z)) a✝¹‖

Tactic:
positivity

Result:
no goals

Proof state:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun z => z⁻¹ / log z ^ 2

Tactic:
refine GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
  (GrowsPolynomially.pow 2 growsPolynomially_log ?_)

Result:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / log z ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ log x

Proof state:
case inr
p : ℝ
hp : p ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ ‖deriv (fun z => z ^ p * (1 + ε z)) x‖

Tactic:
filter_upwards [eventually_gt_atTop 0] with _ _

Result:
case h
p : ℝ
hp : p ≠ 0
a✝¹ : ℝ
a✝ : 0 < a✝¹
⊢ 0 ≤ ‖deriv (fun z => z ^ p * (1 + ε z)) a✝¹‖

Proof state:
case h
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
⊢ ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ = x⁻¹ / log x ^ 2

Tactic:
have : 0 ≤ x⁻¹ / (log x ^ 2) := by
  have hlog : 0 < log x := Real.log_pos hx_pos
  positivity

Result:
case h
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x => 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
this : 0 ≤ x⁻¹ / log x ^ 2
⊢ ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ = x⁻¹ / log x ^ 2