awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑(#(Ico (r i n) n)) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
have e_a : (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
have e_a : (↑(n - r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
Tactic: rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
e_a : (↑(n - r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
⊢ (↑(#(Ico (r i n) n)) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
have e_a₁ : HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ)
Tactic: rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) *
      (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1))
have hbc : HSub.hSub (α := ℝ) (↑n : ℝ) (↑(r i n) : ℝ) ≤ (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * (↑n : ℝ) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) =
    c₂ * (HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) * g (↑n : ℝ)
have rw : HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) =
  c₂ * (HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) * g (↑n : ℝ)
Tactic: rw [← Real.rpow_add_one (by positivity) (p a b)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ c₂ * (HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) * g (↑n : ℝ) =
    c₂ * g (↑n : ℝ)
have rw : c₂ * 1 * g (↑n : ℝ) = c₂ * g (↑n : ℝ)
Tactic: rw [div_self (by positivity), mul_one]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
rw : c₂ * 1 * g (↑n : ℝ) = c₂ * g (↑n : ℝ)
⊢ c₂ * (HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1)) * g (↑n : ℝ) =
    c₂ * g (↑n : ℝ)
have rw₁ : c₂ * g (↑n : ℝ) = c₂ * g (↑n : ℝ)
Tactic: rw [div_self (by positivity), mul_one]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ c₂ * g (↑n : ℝ) ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)
have hbc : c₂ ≤ max c₂ (c₂ / c₁ ^ (p a b + 1))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
⊢ sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)
have calc : sumTransform (p a b) g (r i n) n =
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
Tactic: calc sumTransform (p a b) g (r i n) n
      _ = n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl
      _ ≤ n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by
        gcongr with u hu
        rw [Finset.mem_Ico] at hu
        have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
        refine hn₂ u ?_
        rw [Set.mem_Icc]
        refine ⟨?_, by norm_cast; lia⟩
        calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1
      _ ≤ n ^ (p a b) * (∑ _u ∈ Finset.Ico (r i n) n, c₂ * g n / n ^ ((p a b) + 1)) := by
        gcongr n ^ (p a b) * (Finset.Ico (r i n) n).sum (fun _ => c₂ * g n / ?_) with u hu
        rw [Finset.mem_Ico] at hu
        have : 0 < u := calc
          0 < r i n := by exact hrpos_i
          _ ≤ u := by exact hu.1
        exact rpow_le_rpow_of_nonpos (by positivity)
          (by exact_mod_cast (le_of_lt hu.2)) (le_of_lt hp)
      _ ≤ n ^ p a b * #(Ico (r i n) n) • (c₂ * g n / n ^ (p a b + 1)) := by
        gcongr; exact Finset.sum_le_card_nsmul _ _ _ (fun x _ => by rfl)
      _ = n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / n ^ (p a b + 1)) := by
        rw [nsmul_eq_mul, mul_assoc]
      _ = n ^ (p a b) * (n - r i n) * (c₂ * g n / n ^ ((p a b) + 1)) := by
        congr; rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
      _ ≤ n ^ (p a b) * n * (c₂ * g n / n ^ ((p a b) + 1)) := by
        gcongr; simp only [tsub_le_iff_right, le_add_iff_nonneg_right, Nat.cast_nonneg]
      _ = c₂ * (n ^ ((p a b) + 1) / n ^ ((p a b) + 1)) * g n := by
        rw [← Real.rpow_add_one (by positivity) (p a b)]; ring
      _ = c₂ * g n := by rw [div_self (by positivity), mul_one]
      _ ≤ max c₂ (c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact le_max_left _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g (↑n : ℝ)
hp : p a b + 1 < 0
calc :
  sumTransform (p a b) g (r i n) n =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
⊢ sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)
have calc₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1) ≤
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * ∑ u ∈ Ico (r i n) n, c₂ * g (↑n : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1)
Tactic: calc sumTransform (p a b) g (r i n) n
      _ = n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl
      _ ≤ n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by
        gcongr with u hu
        rw [Finset.mem_Ico] at hu
        have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩
        refine hn₂ u ?_
        rw [Set.mem_Icc]
        refine ⟨?_, by norm_cast; lia⟩
        calc c₁ * n ≤ r i n := by exact hn₁ i
                  _ ≤ u := by exact_mod_cast hu'.1
      _ ≤ n ^ (p a b) * (∑ _u ∈ Finset.Ico (r i n) n, c₂ * g n / n ^ ((p a b) + 1)) := by
        gcongr n ^ (p a b) * (Finset.Ico (r i n) n).sum (fun _ => c₂ * g n / ?_) with u hu
        rw [Finset.mem_Ico] at hu
        have : 0 < u := calc
          0 < r i n := by exact hrpos_i
          _ ≤ u := by exact hu.1
        exact rpow_le_rpow_of_nonpos (by positivity)
          (by exact_mod_cast (le_of_lt hu.2)) (le_of_lt hp)
      _ ≤ n ^ p a b * #(Ico (r i n) n) • (c₂ * g n / n ^ (p a b + 1)) := by
        gcongr; exact Finset.sum_le_card_nsmul _ _ _ (fun x _ => by rfl)
      _ = n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / n ^ (p a b + 1)) := by
        rw [nsmul_eq_mul, mul_assoc]
      _ = n ^ (p a b) * (n - r i n) * (c₂ * g n / n ^ ((p a b) + 1)) := by
        congr; rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
      _ ≤ n ^ (p a b) * n * (c₂ * g n / n ^ ((p a b) + 1)) := by
        gcongr; simp only [tsub_le_iff_right, le_add_iff_nonneg_right, Nat.cast_nonneg]
      _ = c₂ * (n ^ ((p a b) + 1) / n ^ ((p a b) + 1)) * g n := by
        rw [← Real.rpow_add_one (by positivity) (p a b)]; ring
      _ = c₂ * g n := by rw [div_self (by positivity), mul_one]
      _ ≤ max c₂ (c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact le_max_left _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have obtain : ∀ (c₁ : ℝ) (hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁)
  (hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)),
  ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
Tactic: obtain ⟨c₁, hc₁_mem, hc₁⟩ := R.exists_eventually_const_mul_le_r
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have obtain : ∀ (c₂ : ℝ) (hc₂_mem : c₂ > 0)
  (hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u),
  ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
Tactic: obtain ⟨c₂, hc₂_mem, hc₂⟩ := R.g_grows_poly.eventually_atTop_ge_nat hc₁_mem
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have obtain : ∀ (c₃ : ℝ) (hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃)
  (hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)),
  ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
Tactic: obtain ⟨c₃, hc₃_mem, hc₃⟩ := R.exists_eventually_r_le_const_mul
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have hc₁_pos : 0 < c₁
Tactic: have hc₁_pos : 0 < c₁ := hc₁_mem.1
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
⊢ 0 < 1 - c₃
have this : c₃ < 1
Tactic: have := hc₃_mem.2
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
this : c₃ < 1
⊢ 0 < 1 - c₃
have linarith : 1 - c₃ ≤ 0 → c₃ - 1 + (1 - c₃ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have hc₃' : 0 < 1 - c₃
Tactic: have hc₃' : 0 < (1 - c₃) := by have := hc₃_mem.2; linarith
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have refine : ∀ᶠ (n : ℕ) in atTop,
  ∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
Tactic: refine ⟨min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁^((p a b) + 1)), by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (i : α), min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have h : ∀ (n : ℕ) (hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ))
  (hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u)
  (hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)) (hrpos : ∀ (i : α), 0 < r i n) (hr_lt_n : ∀ (i : α), r i n < n)
  (hn_pos : 0 < n) (i : α),
  min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
Tactic: filter_upwards [hc₁, hc₂, hc₃, R.eventually_r_pos, R.eventually_r_lt_n, eventually_gt_atTop 0]
    with n hn₁ hn₂ hn₃ hrpos hr_lt_n hn_pos
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
⊢ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have hrpos_i : 0 < r i n
Tactic: have hrpos_i := hrpos i
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
c₃ : ℝ
hc₃_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
hn₂ : ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), c₂ * g (↑n : ℝ) ≤ g u
hn₃ : ∀ (i : α), (↑(r i n) : ℝ) ≤ c₃ * (↑n : ℝ)
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
⊢ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ) ≤ sumTransform (p a b) g (r i n) n
have g_nonneg : 0 ≤ g (↑n : ℝ)
Tactic: have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity)