awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = -deriv ε x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = -deriv ε x
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
Tactic: rw [deriv_fun_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = -deriv ε x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = -deriv ε x
have h₂ : DifferentiableAt ℝ ε x
Tactic: rw [deriv_fun_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -deriv ε z) fun (x : ℝ) ↦ x⁻¹
have rw : IsLittleO (F := ℝ) atTop (deriv ε) fun (x : ℝ) ↦ x⁻¹
Tactic: rw [isLittleO_neg_left]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (x : ℝ) ↦ 1 + ε x) fun (z : ℝ) ↦ deriv ε z
have h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε (↑n : ℝ)
have h₁ : IsLittleO (F := ℝ) atTop ε fun (x : ℝ) ↦ 1
Tactic: have h₁ := isLittleO_smoothingFn_one
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
h₁ : IsLittleO (F := ℝ) atTop ε fun (x : ℝ) ↦ 1
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε (↑n : ℝ)
have h₂ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
Tactic: rw [isLittleO_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε (↑n : ℝ)
have refine : ∀ᶠ (x : ℝ) in atTop, (fun (n : ℝ) ↦ 0 < 1 + ε n) x
Tactic: refine Eventually.natCast_atTop (p := fun n => 0 < 1 + ε n) ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
⊢ ∀ᶠ (x : ℝ) in atTop, (fun (n : ℝ) ↦ 0 < 1 + ε n) x
have h : ∀ (x : ℝ), ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1 → ∀ (hx' : 1 < x), 0 < 1 + ε x
Tactic: filter_upwards [h₁ (by simp : (0 : ℝ) < 1 / 2), eventually_gt_atTop 1] with x _ hx'
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
x : ℝ
h : ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1
hx' : 1 < x
⊢ 0 < 1 + ε x
have this : 0 < log x
Tactic: have : 0 < log x := Real.log_pos hx'
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 + ε (↑(r i n) : ℝ)
have rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 + ε (↑(r i x) : ℝ)
Tactic: rw [Filter.eventually_all]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 + ε (↑n : ℝ)
have h : ∀ (n : ℕ) (hn : 0 < 1 + ε (↑n : ℝ)), 0 ≤ 1 + ε (↑n : ℝ)
Tactic: filter_upwards [eventually_one_add_smoothingFn_pos] with n hn
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ 1 / log x) (Set.Ioi 1)
have simp_rw : StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (Set.Ioi 1)
Tactic: simp_rw [one_div]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (Set.Ioi 1)
have log : StrictMonoOn log (Set.Ioi 1)
Tactic: refine StrictAntiOn.comp_strictMonoOn inv_strictAntiOn ?log fun _ hx => log_pos hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ StrictMonoOn log (Set.Ioi 1)
have log : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioi 1) x), Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
Tactic: refine StrictMonoOn.mono strictMonoOn_log (fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
have h : ∀ (n : ℕ) (hn : 1 < n) (hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))),
  1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ) =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
Tactic: filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
⊢ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ) =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
have h_log_pos : 0 < log (↑n : ℝ)
Tactic: have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
⊢ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ) =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
have h : (log (b i * (↑n : ℝ)))⁻¹ - (log (↑n : ℝ))⁻¹ =
  (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
Tactic: simp only [one_div]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
⊢ log (b i * (↑n : ℝ)) ≠ 0
have this : 0 < log (b i * (↑n : ℝ))
Tactic: have := hn' i
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
⊢ (log (b i * (↑n : ℝ)))⁻¹ - (log (↑n : ℝ))⁻¹ =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
have h : (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
  (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
Tactic: rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
have h : ∀ (n : ℕ) (hn : n ≠ 0),
  (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
⊢ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
have this : 0 < b i
Tactic: have : 0 < b i := R.b_pos i
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
have h : (log (↑n : ℝ) - (log (b i) + log (↑n : ℝ))) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)) =
  (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
Tactic: rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
h :
  (log (↑n : ℝ) - (log (b i) + log (↑n : ℝ))) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
⊢ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
have h₁ : (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)) =
  (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
Tactic: rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ Eq (α := (n : ℕ) → ℝ)
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)))
    fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
have h : ∀ (x : ℕ),
  (log (↑x : ℝ) - log (b i) - log (↑x : ℝ)) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ)) =
    -log (b i) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x : ℕ
⊢ (log (↑x : ℝ) - log (b i) - log (↑x : ℝ)) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ)) =
    -log (b i) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ))
have h : log (↑x : ℝ) - log (b i) - log (↑x : ℝ) = -log (b i)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))
have refine : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ)
Tactic: refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)
have h : ∀ (x : ℕ), log (b i) + log (↑x : ℝ) = log (↑x : ℝ) + log (b i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ)
have this : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)
Tactic: have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
this : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ)
have rw : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)) fun (n : ℕ) ↦ log (↑n : ℝ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have h : ∀ (x : ℕ), -log (b i) / (log (↑x : ℝ) * log (↑x : ℝ)) = -log (b i) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x : ℕ
⊢ -log (b i) / (log (↑x : ℝ) * log (↑x : ℝ)) = -log (b i) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
have h : log (↑x : ℝ) * log (↑x : ℝ) = HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x : ℕ
⊢ log (↑x : ℝ) * log (↑x : ℝ) = HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
have h : HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2 = HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
Tactic: rw [← pow_two]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc : EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
  (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
Tactic: calc (fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
calc :
  EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₁ : EventuallyEq (β := ℝ) atTop
  (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
  (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
Tactic: calc (fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
calc :
  EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
calc₁ :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₂ : Eq (α := (n : ℕ) → ℝ)
  (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
  -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
Tactic: calc (fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
calc :
  EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
calc₁ :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
calc₂ :
  Eq (α := (n : ℕ) → ℝ)
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)))
    fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₃ : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
  -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))
Tactic: calc (fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]