-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isTheta_smoothingFn_sub_self (i : α) :
    (fun (n : ℕ) => ε (b i * n) - ε n) =Θ[atTop] fun n => 1 / (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 => ε (b i * ↑n) - ε ↑n) =Θ[atTop] fun n => -log (b i) / log ↑n ^ 2

Tactic:
exact (R.isEquivalent_smoothingFn_sub_self i).isTheta

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 : α
⊢ log (b i) ≠ 0

Tactic:
exact Real.log_ne_zero_of_pos_of_ne_one
        (R.b_pos i) (ne_of_lt <| R.b_lt_one i)

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 : α
this : -log (b i) ≠ 0
⊢ (fun n => -log (b i) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n => 1 / log ↑n ^ 2

Tactic:
rw [← isTheta_const_mul_right this]

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 : α
⊢ -log (b i) ≠ 0

Tactic:
rw [neg_ne_zero]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ log (b i) ≠ 0

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) * 1 / log ↑n ^ 2) = fun n => -log (b i) * (1 / log ↑n ^ 2)

Tactic:
simp_rw [← mul_div_assoc]

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 ^ 2) = fun n => -log (b i) * 1 / log ↑n ^ 2

Tactic:
simp only [mul_one]

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) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n => 1 / log ↑n ^ 2

Tactic:
have : -log (b i) ≠ 0 := by
  rw [neg_ne_zero]
  exact Real.log_ne_zero_of_pos_of_ne_one
          (R.b_pos i) (ne_of_lt <| R.b_lt_one i)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
this : -log (b i) ≠ 0
⊢ (fun n => -log (b i) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n => 1 / 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 => ε (b i * ↑n) - ε ↑n) =Θ[atTop] fun n => 1 / log ↑n ^ 2

Tactic:
calc (fun (n : ℕ) => ε (b i * n) - ε n) =Θ[atTop] fun n => (-log (b i)) / (log n)^2 := by
                exact (R.isEquivalent_smoothingFn_sub_self i).isTheta
  _ = fun (n : ℕ) => (-log (b i)) * 1 / (log n)^2 := by simp only [mul_one]
  _ = fun (n : ℕ) => -log (b i) * (1 / (log n)^2) := by simp_rw [← mul_div_assoc]
  _ =Θ[atTop] fun (n : ℕ) => 1 / (log n)^2 := by
                have : -log (b i) ≠ 0 := by
                  rw [neg_ne_zero]
                  exact Real.log_ne_zero_of_pos_of_ne_one
                          (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
                rw [← isTheta_const_mul_right this]

Result:
no goals