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
i : α
calc :
  EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
calc₁ :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
calc₂ :
  Eq (α := (n : ℕ) → ℝ)
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)))
    fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
calc₃ :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₄ : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))) fun (n : ℕ) ↦
  -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: calc (fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]
-- 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
i : α
⊢ -log (b i) ≠ 0
have rw : log (b i) ≠ 0
Tactic: rw [neg_ne_zero]
-- 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
i : α
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have this : -log (b i) ≠ 0
Tactic: have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one 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
i : α
this : -log (b i) ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have rw : IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)) fun (n : ℕ) ↦
  -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)
Tactic: rw [← isTheta_const_mul_right this]
-- 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
i : α
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
  -log (b i) * 1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: calc (fun (n : ℕ) => ε (b i * n) - ε n)
    _ =Θ[atTop] fun n => (-log (b i)) / (log n) ^ 2 :=
      (R.isEquivalent_smoothingFn_sub_self i).isTheta
    _ = fun (n : ℕ) => (-log (b i)) * 1 / (log n) ^ 2 := by simp only [mul_one]
    _ = fun (n : ℕ) => -log (b i) * (1 / (log n) ^ 2) := by simp_rw [← mul_div_assoc]
    _ =Θ[atTop] fun (n : ℕ) => 1 / (log n) ^ 2 := by
      have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
      rw [← isTheta_const_mul_right this]
-- 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
i : α
calc :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    -log (b i) * 1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₁ : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) * 1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
  -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)
Tactic: calc (fun (n : ℕ) => ε (b i * n) - ε n)
    _ =Θ[atTop] fun n => (-log (b i)) / (log n) ^ 2 :=
      (R.isEquivalent_smoothingFn_sub_self i).isTheta
    _ = fun (n : ℕ) => (-log (b i)) * 1 / (log n) ^ 2 := by simp only [mul_one]
    _ = fun (n : ℕ) => -log (b i) * (1 / (log n) ^ 2) := by simp_rw [← mul_div_assoc]
    _ =Θ[atTop] fun (n : ℕ) => 1 / (log n) ^ 2 := by
      have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
      rw [← isTheta_const_mul_right this]
-- 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
i : α
calc :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    -log (b i) * 1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
calc₁ :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) * 1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₂ : IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)) fun (n : ℕ) ↦
  1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: calc (fun (n : ℕ) => ε (b i * n) - ε n)
    _ =Θ[atTop] fun n => (-log (b i)) / (log n) ^ 2 :=
      (R.isEquivalent_smoothingFn_sub_self i).isTheta
    _ = fun (n : ℕ) => (-log (b i)) * 1 / (log n) ^ 2 := by simp only [mul_one]
    _ = fun (n : ℕ) => -log (b i) * (1 / (log n) ^ 2) := by simp_rw [← mul_div_assoc]
    _ =Θ[atTop] fun (n : ℕ) => 1 / (log n) ^ 2 := by
      have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
      rw [← isTheta_const_mul_right this]
-- 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
⊢ Continuous (Y := ℝ) fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p
have refine : ∀ (i : α), Membership.mem (γ := Finset α) univ i → Continuous (X := ℝ) (HPow.hPow (b i))
Tactic: refine continuous_finsetSum Finset.univ fun i _ => Continuous.mul (by fun_prop) ?_
-- 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
⊢ StrictAnti (β := ℝ) fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p
have rw : StrictAnti (α := ℝ) (β := ℝ) (∑ c : α, fun (p : ℝ) ↦ a c * b c ^ p)
Tactic: rw [← Finset.sum_fn]
-- 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
⊢ StrictAnti (α := ℝ) (β := ℝ) (∑ c : α, fun (p : ℝ) ↦ a c * b c ^ p)
have terms : ∀ (x : α), Membership.mem (γ := Finset α) univ x → StrictAnti (β := ℝ) fun (p : ℝ) ↦ a x * b x ^ p
Tactic: refine Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms
-- 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
⊢ ∀ (x : α), Membership.mem (γ := Finset α) univ x → StrictAnti (β := ℝ) fun (p : ℝ) ↦ a x * b x ^ p
have terms : ∀ (i : α), Membership.mem (γ := Finset α) univ i → StrictAnti (α := ℝ) (HPow.hPow (b i))
Tactic: refine fun i _ => StrictAnti.const_mul ?_ (R.a_pos 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
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 0)
have h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
Tactic: have h₁ : Finset.univ.sum (fun _ : α => (0 : ℝ)) = 0 := by simp
-- 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 (∑ x : α, 0))
Tactic: rw [← h₁]
-- 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 (∑ x : α, 0))
have refine : ∀ (i : α), Membership.mem (γ := Finset α) univ i → Tendsto (β := ℝ) (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 0)
Tactic: refine tendsto_finsetSum (univ : Finset α) (fun 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 0)
have rw : Tendsto (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 (a i * 0))
Tactic: rw [← mul_zero (a 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ Tendsto (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 (a i * 0))
have refine : -1 < b i
Tactic: refine Tendsto.mul (by simp) <| tendsto_rpow_atTop_of_base_lt_one _ ?_ (R.b_lt_one 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ -1 < b i
have this : 0 < b i
Tactic: have := R.b_pos 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
this : 0 < b i
⊢ -1 < b i
have linarith : b i ≤ -1 → -1 + (0 - b i) + (b i - -1) = 0
Tactic: 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
this : 0 < b (max_bi b)
⊢ 0 < b (max_bi b)
have linarith : b (max_bi b) ≤ 0 → 0 - b (max_bi b) + (b (max_bi b) - 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
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atBot atTop
have h₁ : Tendsto (β := ℝ) (fun (p : ℝ) ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
Tactic: have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
    Tendsto.const_mul_atTop (R.a_pos (max_bi b)) <| tendsto_rpow_atBot_of_base_lt_one _
      (by have := R.b_pos (max_bi b); linarith) (R.b_lt_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
h₁ : Tendsto (β := ℝ) (fun (p : ℝ) ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atBot atTop
have refine : ∀ (p : ℝ), a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p
Tactic: refine tendsto_atTop_mono (fun p => ?_) h₁
-- 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
h₁ : Tendsto (β := ℝ) (fun (p : ℝ) ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
⊢ a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p
have refine : ∀ (i : α), Membership.mem (γ := Finset α) univ i → LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
Tactic: refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)
-- 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
h₁ : Tendsto (β := ℝ) (fun (p : ℝ) ↦ a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
have positivity : 0 < a i → LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
Tactic: positivity [R.a_pos i, R.b_pos 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
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)
⊢ LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
have positivity₃ : 0 < a i → 0 < b i → LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
Tactic: positivity [R.a_pos i, R.b_pos 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
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1
have refine : ∃ (a_1 : ℝ), LE.le (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1
Tactic: refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_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
refine : ∃ (a_1 : ℝ), LE.le (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1
have refine₁ : ∃ (b_1 : ℝ), LE.le (α := ℝ) 1 (∑ i : α, a i * b i ^ b_1)
Tactic: refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_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
⊢ Eq (α := ℝ) (∑ i : α, a i * b i ^ p a b) 1
have simp : Eq (α := ℝ)
  (∑ x : α, a x * HPow.hPow (β := ℝ) (b x) (Function.invFun (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1)) 1
Tactic: simp only [p]
-- 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
⊢ ∃ (a_1 : ℝ), Eq (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1
have rw : Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1
Tactic: rw [← Set.mem_range]
-- 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
rw : Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1
⊢ ∃ (a_1 : ℝ), Eq (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1
have rw₁ : Type
Tactic: rw [← Set.mem_range]
-- 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
rw : Membership.mem (γ := Set ℝ) (Set.range fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) 1
rw₁ rw₂ : Type
rw₃ : ℝ → ℝ
⊢ ∃ (a_1 : ℝ), Eq (α := ℝ) (∑ i : α, a i * b i ^ a_1) 1
have rw₄ : ℝ
Tactic: rw [← Set.mem_range]
-- 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
n : ℕ
hn : 0 < n
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0 ≤ asympBound g a b n
have 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))
Tactic: simp only [asympBound_def']
-- 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
n : ℕ
hn : 0 < n
⊢ 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))
have hbc : LE.le (α := ℝ) 0 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))
Tactic: gcongr n ^ p a b * (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
n : ℕ
hn : 0 < n
⊢ LE.le (α := ℝ) 0 (∑ u ∈ range n, g (↑u : ℝ) / HPow.hPow (α := ℝ) (↑u : ℝ) (p a b + 1))
have this : ∀ x ≥ 0, 0 ≤ g x
Tactic: have := R.g_nonneg
-- 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
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n
have calc : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0
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)
-- 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
n : ℕ
hn : 0 < n
calc : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 0
⊢ 0 < asympBound g a b n
have calc₁ : HPow.hPow (α := ℝ) (↑n : ℝ) (p a b) * HAdd.hAdd (α := ℝ) 1 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)
-- 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
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n
have 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
Tactic: filter_upwards [eventually_gt_atTop 0] with n hn using R.asympBound_pos n hn
-- 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
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
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < asympBound g a b n
have h₁ : ∀ (a_1 : ℕ), 0 < a_1 → 0 < asympBound g a b a_1
Tactic: filter_upwards [eventually_gt_atTop 0] with n hn using R.asympBound_pos n hn
-- 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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < asympBound g a b (r i n)
have rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)
Tactic: rw [Filter.eventually_all]
-- 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 : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑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 : α), 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
-- 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 : α), sumTransform (p a b) g (r i n) n ≤ c * g (↑n : ℝ)
have 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 : ℝ)
Tactic: obtain ⟨c₂, hc₂_mem, hc₂⟩ := R.g_grows_poly.eventually_atTop_le_nat hc₁_mem