-- 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 (b i) + log ↑n) = fun n => log ↑n + log (b i)

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)

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

Tactic:
rw [this]

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

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (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)

Tactic:
filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn 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 : 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)

Proof state:
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

Tactic:
congr 1

Result:
case h.e_a
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ log ↑x✝ * log ↑x✝ = 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 : n ≠ 0
this : 0 < b i
⊢ b i ≠ 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 : α
x✝ : ℕ
⊢ log (b i) + log ↑x✝ = log ↑x✝ + log (b i)

Tactic:
simp [add_comm]

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 : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ ↑n ≠ 0

Tactic:
aesop

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) ~[atTop] fun n => log ↑n

Tactic:
have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
  ext; simp [add_comm]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
this : (fun n => log (b i) + log ↑n) = fun n => log ↑n + log (b i)
⊢ (fun n => log (b i) + log ↑n) ~[atTop] fun n => log ↑n

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

Tactic:
congr

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

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 (b i * ↑n) ≠ 0

Tactic:
have := hn' i

Result:
α : 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

Proof state:
case h.e_a
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ log ↑x✝ - log (b i) - log ↑x✝ = -log (b i)

Tactic:
ring

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
⊢ (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)]

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 : (fun n => log (b i) + log ↑n) = fun n => log ↑n + log (b i)
⊢ (fun n => log ↑n + log (b i)) ~[atTop] fun n => log ↑n

Tactic:
exact IsEquivalent.add_isLittleO IsEquivalent.refl
  <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
    isLittleO_const_log_atTop

Result:
no goals

Proof state:
case h.e_a
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ log ↑x✝ * log ↑x✝ = log ↑x✝ ^ 2

Tactic:
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 : 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:
have : 0 < b i := R.b_pos i

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
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)

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 (b i) + log ↑n) * log ↑n)) ~[atTop] fun n => -log (b i) / (log ↑n * log ↑n)

Tactic:
refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)

Result:
α : 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) ~[atTop] fun 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)
⊢ 1 < ↑n

Tactic:
aesop

Result:
no goals