-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma rpow_p_mul_one_sub_smoothingFn_le :
    ∀ᶠ (n : ℕ) in atTop, ∀ i, (r i n) ^ (p a b) * (1 - ε (r i n))
      ≤ (b i) ^ (p a b) * n ^ (p a b) * (1 - ε n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
h_main_norm :
  (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
⊢ (fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖) =ᶠ[atTop] fun n =>
    b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
filter_upwards [eventually_gt_atTop ⌈(b i)⁻¹⌉₊, eventually_gt_atTop 1] 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 : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
h_main_norm :
  (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
⊢ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖ = b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
⊢ (fun n => ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)

Tactic:
refine IsTheta.symm ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
⊢ (fun n => b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n => ↑n ^ p a b * (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 : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)

Tactic:
have h_main_norm : (fun (n : ℕ) => ‖q (r i n) - q (b i * n)‖)
    ≤ᶠ[atTop] fun (n : ℕ) => ‖(b i) ^ (p a b) * n ^ (p a b) * (ε (b i * n) - ε n)‖ := by
  refine IsLittleO.eventuallyLE ?_
  calc
    (fun (n : ℕ) => q (r i n) - q (b i * n))
        =O[atTop] fun n => (deriv q n) * (r i n - b i * n) := by
            exact R.isBigO_apply_r_sub_b q h_diff_q
              (growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p a b)) i
      _ =o[atTop] fun n => (deriv q n) * (n / log n ^ 2) := by
            exact IsBigO.mul_isLittleO (isBigO_refl _ _) (R.dist_r_b i)
      _ =O[atTop] fun n => n^((p a b) - 1) * (n / log n ^ 2) := by
            exact IsBigO.mul (IsBigO.natCast_atTop h_deriv_q) (isBigO_refl _ _)
      _ =ᶠ[atTop] fun n => n^(p a b) / (log n) ^ 2 := by
            filter_upwards [eventually_ne_atTop 0] with n hn
            have hn' : (n : ℝ) ≠ 0 := by positivity
            simp [← mul_div_assoc, ← Real.rpow_add_one hn']
      _ = fun (n : ℕ) => (n : ℝ) ^ (p a b) * (1 / (log n)^2) := by
            simp_rw [mul_div, mul_one]
      _ =Θ[atTop] fun (n : ℕ) => (b i) ^ (p a b) * n ^ (p a b) * (1 / (log n)^2) := by
            refine IsTheta.symm ?_
            simp_rw [mul_assoc]
            refine IsTheta.const_mul_left ?_ (isTheta_refl _ _)
            have := R.b_pos i; positivity
      _ =Θ[atTop] fun (n : ℕ) => (b i)^(p a b) * n^(p a b) * (ε (b i * n) - ε n) := by
            exact IsTheta.symm <| IsTheta.mul (isTheta_refl _ _)
              <| R.isTheta_smoothingFn_sub_self i

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
h_main_norm :
  (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
h_main_norm :
  (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
this : 0 < b i
⊢ q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
simp only [q, mul_rpow (by positivity : (0 : ℝ) ≤ b i) (by positivity : (0 : ℝ) ≤ n)]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
h_main_norm :
  (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
this : 0 < b i
⊢ b i ^ p a b * ↑n ^ p a b * (1 - ε (b i * ↑n)) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) =
    b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
⊢ (fun n => b i ^ p a b * ↑n ^ p a b * (1 / log ↑n ^ 2)) =Θ[atTop] fun n =>
    b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
exact IsTheta.symm <| IsTheta.mul (isTheta_refl _ _)
  <| R.isTheta_smoothingFn_sub_self 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 : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
⊢ (fun n => ↑n ^ p a b / log ↑n ^ 2) = fun n => ↑n ^ p a b * (1 / log ↑n ^ 2)

Tactic:
simp_rw [mul_div, mul_one]

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 : α
q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)
h_main_norm :
  (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
a✝ : ℕ
⊢ q ↑(r i a✝) - q (b i * ↑a✝) ≤ ‖q ↑(r i a✝) - q (b i * ↑a✝)‖

Tactic:
exact le_norm_self _

Result:
no goals