-- 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)
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
⊢ 0 ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
have h₁ := 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 : α
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
h₁ : 0 < b i
⊢ 0 ≤ 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)
z : ℝ
hz : z ∈ Set.Ioi 1
⊢ z ∈ {0}ᶜ

Tactic:
rw [Set.mem_compl_singleton_iff]

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)
z : ℝ
hz : z ∈ Set.Ioi 1
⊢ z ≠ 0

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

Tactic:
rw [deriv_mul] <;> 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 : α
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)
h₁ : 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)
⊢ q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
rw [← h₁, ← sub_le_iff_le_add']

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)‖
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)
h₁ : 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)
⊢ q ↑(r i n) - q (b i * ↑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)
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)

Tactic:
ring

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 : α), ∀ᶠ (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:
intro i

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (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:
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)‖
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)
h₁ : 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)
⊢ q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)

Tactic:
exact 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)
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
h₁ : 0 < b i
⊢ b i * ↑n ∈ Set.Ioi 1

Tactic:
calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
    _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
    _ < b i * n := by gcongr

Result:
no goals