-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isEquivalent_smoothingFn_sub_self (i : α) :
    (fun (n : ℕ) => ε (b i * n) - ε n) ~[atTop] fun n => -log (b i) / (log n)^2

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n => (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)) =ᶠ[atTop] fun 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

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n => ε (b i * ↑n) - ε ↑n) ~[atTop] fun n => -log (b i) / log ↑n ^ 2

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 aesop
          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 aesop), 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]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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)

Tactic:
have h_log_pos : 0 < log n := Real.log_pos <| by aesop

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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
this : 0 < log (b i * ↑n)
⊢ log (b i * ↑n) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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)

Tactic:
rw [log_mul (by positivity) (by aesop), sub_add_eq_sub_sub]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n => -log (b i) / (log ↑n * log ↑n)) = fun n => -log (b i) / log ↑n ^ 2

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ -log (b i) / (log ↑x✝ * log ↑x✝) = -log (b i) / log ↑x✝ ^ 2

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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 ↑n ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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)

Tactic:
simp only [one_div]

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : 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)