-- 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:
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)
n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2

Tactic:
simp [← mul_div_assoc, ← Real.rpow_add_one hn']

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)
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

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)
⊢ (deriv fun x => (fun z => z ^ p a b) x * (fun z => 1 - ε z) x) =ᶠ[atTop] fun x =>
    deriv (fun z => z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z => 1 - ε z) x

Tactic:
filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'

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)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ deriv (fun x => x ^ p a b * (1 - ε x)) x =
    deriv (fun z => z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z => 1 - ε z) 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)
z : ℝ
hz : 1 < z
⊢ z ≠ 0

Tactic:
exact ne_of_gt <| zero_lt_one.trans hz

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)
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2

Tactic:
have hn' : (n : ℝ) ≠ 0 := by positivity

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)
n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / 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)
⊢ ∀ᶠ (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_deriv_q : deriv q =O[atTop] fun x => x ^ ((p a b) - 1) := calc
  deriv q = deriv fun x => (fun z => z ^ (p a b)) x * (fun z => 1 - ε z) x := by rfl
        _ =ᶠ[atTop] fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x) +
                x ^ (p a b) * deriv (fun z => 1 - ε z) x := by
            filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'
            rw [deriv_mul] <;> aesop
        _ =O[atTop] fun x => x ^ ((p a b) - 1) := by
            refine IsBigO.add ?left ?right
            case left => calc
              (fun x => deriv (fun z => z ^ (p a b)) x * (1 - ε x))
                  =O[atTop] fun x => x ^ ((p a b) - 1) * (1 - ε x) := by
                    exact IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _)
                _ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 := by
                    refine IsBigO.mul (isBigO_refl _ _)
                      isEquivalent_one_sub_smoothingFn_one.isBigO
                _ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]
            case right => calc
              (fun x => x ^ (p a b) * deriv (fun z => 1 - ε z) x)
                  =O[atTop] (fun x => x ^ (p a b) * x⁻¹) := by
                    exact IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_sub_smoothingFn.isBigO
                _ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) := by
                    filter_upwards [eventually_gt_atTop 0] with x hx
                    rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

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)
⊢ ∀ᶠ (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)
⊢ (fun x => x ^ p a b * deriv (fun z => 1 - ε z) x) =O[atTop] fun x => x ^ p a b * x⁻¹

Tactic:
exact IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_sub_smoothingFn.isBigO

Result:
no goals