awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (β := ℝ) (fun (p : ℝ) ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
h : Membership.mem (γ := Finset α) univ i
positivity positivity₁ positivity₂ : 0 < a i → LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
positivity₃ positivity₄ : 0 < a i → 0 < b i → LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
⊢ LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)

Tactic:
positivity [R.a_pos i, R.b_pos i]

Premises used: AkraBazziRecurrence.a_pos, AkraBazziRecurrence.b_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1

Tactic:
mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_one

Premises used: AkraBazziRecurrence.continuous_sumCoeffsExp, mem_range_of_exists_le_of_exists_ge
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
refine : ∃ (a_1 : ℝ), LE.le (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1
refine₁ : ∃ (b_1 : ℝ), LE.le (α := ℝ) 1 (∑ i : α, a i * b i ^ b_1)
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1

Tactic:
refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_one

Premises used: AkraBazziRecurrence.continuous_sumCoeffsExp, mem_range_of_exists_le_of_exists_ge
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ (a_1 : ℝ), LE.le (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1

Tactic:
R.tendsto_zero_sumCoeffsExp.eventually_le_const zero_lt_one |>.exists

Premises used: AkraBazziRecurrence.tendsto_zero_sumCoeffsExp, Filter.Tendsto.eventually_le_const, Filter.Eventually.exists, zero_lt_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ (a_1 : ℝ), LE.le (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1

Tactic:
exact R.tendsto_zero_sumCoeffsExp.eventually_le_const zero_lt_one |>.exists

Premises used: AkraBazziRecurrence.tendsto_zero_sumCoeffsExp, Filter.Tendsto.eventually_le_const, Filter.Eventually.exists, zero_lt_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ (a_1 : ℝ), LE.le (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1

Tactic:
case le_one =>
    exact R.tendsto_zero_sumCoeffsExp.eventually_le_const zero_lt_one |>.exists

Premises used: AkraBazziRecurrence.tendsto_zero_sumCoeffsExp, Filter.Tendsto.eventually_le_const, Filter.Eventually.exists, zero_lt_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ (b_1 : ℝ), LE.le (α := ℝ) 1 (∑ i : α, a i * b i ^ b_1)

Tactic:
R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists

Premises used: AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp, Filter.Eventually.exists, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ (b_1 : ℝ), LE.le (α := ℝ) 1 (∑ i : α, a i * b i ^ b_1)

Tactic:
exact R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists

Premises used: AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp, Filter.Eventually.exists, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ (b_1 : ℝ), LE.le (α := ℝ) 1 (∑ i : α, a i * b i ^ b_1)

Tactic:
case ge_one =>
    exact R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists

Premises used: AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp, Filter.Eventually.exists, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Function.Injective (β := ℝ) fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p

Tactic:
R.strictAnti_sumCoeffsExp.injective

Premises used: AkraBazziRecurrence.strictAnti_sumCoeffsExp, StrictAnti.injective
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
simp :
  Eq (α := ℝ)
    (∑ x : α, a x * HPow.hPow (β := ℝ) (b x) (Function.invFun (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1)) 1
⊢ Eq (α := ℝ) (∑ i : α, a i * b i ^ p a b) 1

Tactic:
simp only [p]

Premises used: AkraBazziRecurrence.p
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
rw : Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1
rw₁ rw₂ : Type
rw₃ : ℝ → ℝ
rw₄ : ℝ
⊢ ∃ (a_1 : ℝ), Eq (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1

Tactic:
rw [← Set.mem_range]

Premises used: Set.mem_range
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1

Tactic:
R.one_mem_range_sumCoeffsExp

Premises used: AkraBazziRecurrence.one_mem_range_sumCoeffsExp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Eq (α := ℝ)
    (∑ x : α, a x * HPow.hPow (β := ℝ) (b x) (Function.invFun (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1)) 1

Tactic:
exact Function.invFun_eq (by rw [← Set.mem_range]; exact R.one_mem_range_sumCoeffsExp)

Premises used: Function.invFun_eq
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
p : ℝ
g : ℝ → ℝ
n₀ n : ℕ
⊢ sumTransform p g n₀ n =
    HPow.hPow (α := ℝ) (↑n : ℝ) p * ∑ u ∈ Ico n₀ n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p + 1)

Tactic:
rfl

Premises used: AkraBazziRecurrence.sumTransform, rfl
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
g : ℝ → ℝ
α : Type u_2
inst : Fintype α
a b : α → ℝ
n : ℕ
⊢ asympBound g a b n = HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) + sumTransform (p a b) g 0 n

Tactic:
rfl

Premises used: AkraBazziRecurrence.asympBound, rfl
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
g : ℝ → ℝ
α : Type u_2
inst : Fintype α
a b : α → ℝ
n : ℕ
⊢ asympBound g a b n =
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      HAdd.hAdd (α := ℝ) 1 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))

Tactic:
simp [asympBound_def, sumTransform, mul_add, mul_one]

Premises used: AkraBazziRecurrence.asympBound_def, AkraBazziRecurrence.sumTransform, mul_add, mul_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0

Tactic:
aesop (add safe Real.rpow_pos_of_pos)

Premises used: Real.rpow_pos_of_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
simp :
  HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0 ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      HAdd.hAdd (α := ℝ) 1 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0 ≤ asympBound g a b n

Tactic:
simp only [asympBound_def']

Premises used: AkraBazziRecurrence.asympBound_def'
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
hbc : LE.le (α := ℝ) 0 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0 ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) *
      HAdd.hAdd (α := ℝ) 1 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))

Tactic:
gcongr n ^ p a b * (1 + ?_)

Premises used: AkraBazziRecurrence.p, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ ∀ x ≥ 0, 0 ≤ g x

Tactic:
have := R.g_nonneg
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ LE.le (α := ℝ) 0 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))

Tactic:
aesop (add safe Real.rpow_nonneg, safe div_nonneg, safe Finset.sum_nonneg)

Premises used: Finset.sum_nonneg, div_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
calc : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0
calc₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0 ≤ asympBound g a b n
⊢ 0 < asympBound g a b n

Tactic:
calc 0 < (n : ℝ) ^ p a b * (1 + 0) := by aesop (add safe Real.rpow_pos_of_pos)
       _ ≤ asympBound g a b n := by
        simp only [asympBound_def']
        gcongr n ^ p a b * (1 + ?_)
        have := R.g_nonneg
        aesop (add safe Real.rpow_nonneg, safe div_nonneg, safe Finset.sum_nonneg)

Premises used: AkraBazziRecurrence.asympBound, Nat.cast, AkraBazziRecurrence.p, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n

Tactic:
R.asympBound_pos n hn

Premises used: AkraBazziRecurrence.asympBound_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
h :
  ∀ (a_1 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ 0 < asympBound g a b n) x} x}
      a_1
h₁ h₂ : ∀ (n : ℕ) (hn : 0 < n), 0 < asympBound g a b n
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n

Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn using R.asympBound_pos n hn

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < asympBound g a b (r i n)

Tactic:
rw [Filter.eventually_all]

Premises used: Filter.eventually_all
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)

Tactic:
fun i => (R.tendsto_atTop_r i).eventually R.eventually_asympBound_pos

Premises used: AkraBazziRecurrence.tendsto_atTop_r, AkraBazziRecurrence.eventually_asympBound_pos, Filter.Tendsto.eventually
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually R.eventually_asympBound_pos

Premises used: AkraBazziRecurrence.tendsto_atTop_r, AkraBazziRecurrence.eventually_asympBound_pos, Filter.Tendsto.eventually
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
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 : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑n : ℝ)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑n : ℝ)

Tactic:
obtain ⟨c₁, hc₁_mem, hc₁⟩ := R.exists_eventually_const_mul_le_r

Premises used: AkraBazziRecurrence.exists_eventually_const_mul_le_r
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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) : ℝ)
obtain :
  ∀ (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * (↑n : ℝ)) (↑n : ℝ), g u ≤ c₂ * g (↑n : ℝ)),
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑n : ℝ)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑n : ℝ)

Tactic:
obtain ⟨c₂, hc₂_mem, hc₂⟩ := R.g_grows_poly.eventually_atTop_le_nat hc₁_mem

Premises used: AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le_nat, AkraBazziRecurrence.g_grows_poly
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : ℝ)
⊢ 0 < c₁

Tactic:
have hc₁_pos : 0 < c₁ := hc₁_mem.1
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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₁
⊢ max c₂ (c₂ / c₁ ^ (p a b + 1)) > 0

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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₁
refine : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑n : ℝ)

Tactic:
refine ⟨max c₂ (c₂ / c₁ ^ (p a b + 1)), by positivity, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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₁
h :
  ∀ (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 : α),
    sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)

Tactic:
filter_upwards [hc₁, hc₂, R.eventually_r_pos, R.eventually_r_lt_n, eventually_gt_atTop 0]
    with n hn₁ hn₂ hrpos hr_lt_n hn_pos i

Premises used: AkraBazziRecurrence.eventually_r_lt_n, AkraBazziRecurrence.eventually_r_pos, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : α
⊢ 0 < r i n

Tactic:
have hrpos_i := hrpos i
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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
⊢ GE.ge (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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
⊢ 0 ≤ g (↑n : ℝ)

Tactic:
have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity)
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : 0 ≤ p a b + 1
⊢ 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:
rfl
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : 0 ≤ p a b + 1
hbc : ∀ (u : ℕ) (hu : u ∈ Ico (r i n) n), g (↑u : ℝ) ≤ c₂ * g (↑n : ℝ)
⊢ 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:
gcongr with u hu
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ r i n ≤ u ∧ u < n

Tactic:
rw [Finset.mem_Ico] at hu

Premises used: Finset.mem_Ico
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ u ≤ n

Tactic:
lia
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ u ∈ Set.Icc (r i n) n

Tactic:
have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by lia⟩