mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
⊢ ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑n‖ →
    (∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)) → ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑n‖
⊢ (∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)) → ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
⊢ ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖ →
    (∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2) → ∀ (i : α), ↑(r i n) ≤ c * ↑n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
⊢ (∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2) → ∀ (i : α), ↑(r i n) ≤ c * ↑n
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
⊢ (∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)) →
    (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
      R.n₀ ≤ n → 0 < n → 1 < b' * ↑n → ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑n)‖

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
⊢ (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
    R.n₀ ≤ n → 0 < n → 1 < b' * ↑n → ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑n)‖
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: n : ℕ
⊢ 0 < 1 - ε ↑n → 0 ≤ 1 - ε ↑n

Tactic:
hn

Goal state after:
n : ℕ
hn : 0 < 1 - ε ↑n
⊢ 0 ≤ 1 - ε ↑n
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 : ℕ
⊢ n ≠ 0 → ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2

Tactic:
hn

Goal state after:
α : 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
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: n : ℕ
⊢ 0 < 1 + ε ↑n → 0 ≤ 1 + ε ↑n

Tactic:
hn

Goal state after:
n : ℕ
hn : 0 < 1 + ε ↑n
⊢ 0 ≤ 1 + ε ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
⊢ (∀ (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)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 : ℕ
⊢ ⌈(b i)⁻¹⌉₊ < n →
    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)

Tactic:
hn

Goal state after:
α : 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
⊢ 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)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
⊢ 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:
hn

Goal state after:
α : 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)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
a✝² : n ≥ 1
a✝¹ : ∀ z ∈ Set.Ico (max n₀ 2) (2 ^ n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
a✝ : z ∈ Set.Ico (2 ^ n * max n₀ 2) (2 ^ (n + 1) * max n₀ 2)
⊢ 1 ≤ 2

Tactic:
norm_num1

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ 1 ∈ Set.range fun p ↦ ∑ i, a i * b i ^ p

Tactic:
refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_one

Goal state after:
case le_one
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ a_1, ∑ i, a i * b i ^ a_1 ≤ 1

case ge_one
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ b_1, 1 ≤ ∑ i, a i * b i ^ b_1
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 : ℕ
⊢ q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) →
    ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
hn

Goal state after:
α : 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)
⊢ ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
⊢ 0 < n → 0 < asympBound g a b n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 : ℕ
⊢ n ≠ 0 → ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2

Tactic:
hn

Goal state after:
α : 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
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 : ℕ
⊢ ⌈(b i)⁻¹⌉₊ < n →
    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)

Tactic:
hn

Goal state after:
α : 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
⊢ 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)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₁
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |g x|) u ∈ Set.Icc (c₃ * (fun x ↦ |g x|) x) (c₄ * (fun x ↦ |g x|) x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * |f x| ≤ |f u|

Tactic:
exact (hf u hu).1

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : 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 (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
⊢ q (b i * ↑n) - q ↑(r 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) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))

Tactic:
hn

Goal state after:
α : 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 (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r 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) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
⊢ 0 < asympBound g a b n → 0 < 1 - ε ↑n → 0 < (1 - ε ↑n) * asympBound g a b n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < asympBound g a b n
⊢ 0 < 1 - ε ↑n → 0 < (1 - ε ↑n) * asympBound g a b n
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
⊢ n₀ ≤ n →
    (∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)) →
      0 < 1 - ε ↑n →
        (∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n) →
          1 / 2 < 1 - ε ↑n →
            (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
              ⌈↑n₀ / b'⌉₊ ≤ n →
                ∀ C ≥ 2 * c₁⁻¹,
                  (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) →
                    T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
⊢ (∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)) →
    0 < 1 - ε ↑n →
      (∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n) →
        1 / 2 < 1 - ε ↑n →
          (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
            ⌈↑n₀ / b'⌉₊ ≤ n →
              ∀ C ≥ 2 * c₁⁻¹,
                (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) →
                  T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₁
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₁ * f x ≤ f u

Tactic:
exact (hf u hu).1

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
⊢ Code.id.eval n = Part.some n

Tactic:
simp! [Seq.seq, Code.id]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, a i * (C * ((1 - ε ↑(r i n)) * (↑(r i n) ^ p a b * (1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1))))) + g ↑n =
    ∑ i, C * a i * (↑(r i n) ^ p a b * (1 - ε ↑(r i n)) * (1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1))) + g ↑n

Tactic:
by
      congr; ext; ring

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
_ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
           _ ≤ f x + 1 / 2 * f x := by gcongr
           _ = 3 / 2 * f x := by ring

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i,
        C * a i *
          (b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n) *
            (1 + (∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1) - ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1)))) +
      g ↑n =
    ∑ i,
        C * a i *
          (b i ^ p a b * (1 - ε ↑n) *
            (↑n ^ p a b * (1 + ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)) -
              ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1))) +
      g ↑n

Tactic:
by
      congr; ext; ring

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, C * a i * (b i ^ p a b * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n)) + g ↑n =
    ∑ i, C * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n) * (a i * b i ^ p a b) + g ↑n

Tactic:
by
      congr; ext; ring

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
⊢ 0 < asympBound g a b n → 0 < 1 + ε ↑n → 0 ≤ (1 + ε ↑n) * asympBound g a b n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < asympBound g a b n
⊢ 0 < 1 + ε ↑n → 0 ≤ (1 + ε ↑n) * asympBound g a b n