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
i : α
h : ∀ (x : ℕ), log (b i) + log (↑x : ℝ) = log (↑x : ℝ) + log (b i)
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)

Tactic:
ext
-- 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 : ℕ
⊢ log (b i) + log (↑x : ℝ) = log (↑x : ℝ) + log (b i)

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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 : α
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)

Tactic:
have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
-- 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 : α
this : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)
rw : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)) fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ)

Tactic:
rw [this]
-- 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 : α
this : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)) fun (n : ℕ) ↦ log (↑n : ℝ)

Tactic:
IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop

Premises used: Asymptotics.IsEquivalent.add_isLittleO, Real.isLittleO_const_log_atTop, Asymptotics.IsEquivalent.refl, Asymptotics.IsLittleO.natCast_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
i : α
this : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (↑n : ℝ) + log (b i)) fun (n : ℕ) ↦ log (↑n : ℝ)

Tactic:
exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop

Premises used: Asymptotics.IsEquivalent.add_isLittleO, Real.isLittleO_const_log_atTop, Asymptotics.IsEquivalent.refl, Asymptotics.IsLittleO.natCast_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
i : α
h : ∀ (x : ℕ), -log (b i) / (log (↑x : ℝ) * log (↑x : ℝ)) = -log (b i) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
ext
-- 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 : ℕ
h : log (↑x : ℝ) * log (↑x : ℝ) = HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
⊢ -log (b i) / (log (↑x : ℝ) * log (↑x : ℝ)) = -log (b i) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2

Tactic:
congr 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
i : α
x : ℕ
h h₁ : HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2 = HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
⊢ log (↑x : ℝ) * log (↑x : ℝ) = HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2

Tactic:
rw [← pow_two]

Premises used: pow_two
-- 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 : α
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 : ℝ))
calc₄ :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑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]

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, Real.log, Filter.atTop, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- 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 : α
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) fun (n : ℕ) ↦
    -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
(R.isEquivalent_smoothingFn_sub_self i).isTheta

Premises used: AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self, Asymptotics.IsEquivalent.isTheta
-- 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 : α
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ -log (b i) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    -log (b i) * 1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
simp only [mul_one]

Premises used: 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
i : α
⊢ 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:
simp_rw [← mul_div_assoc]

Premises used: mul_div_assoc
-- 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 : α
rw : log (b i) ≠ 0
⊢ -log (b i) ≠ 0

Tactic:
rw [neg_ne_zero]

Premises used: neg_ne_zero
-- 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 : α
⊢ log (b i) ≠ 0

Tactic:
Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)

Premises used: AkraBazziRecurrence.b_pos, AkraBazziRecurrence.b_lt_one, ne_of_lt, Real.log_ne_zero_of_pos_of_ne_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
i : α
⊢ log (b i) ≠ 0

Tactic:
exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)

Premises used: AkraBazziRecurrence.b_pos, AkraBazziRecurrence.b_lt_one, ne_of_lt, Real.log_ne_zero_of_pos_of_ne_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
i : α
⊢ -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)
-- 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 : α
this : -log (b i) ≠ 0
rw 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)
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
rw [← isTheta_const_mul_right this]

Premises used: Asymptotics.isTheta_const_mul_right
-- 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 : α
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)
calc₂ :
  IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) * (1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)) fun (n : ℕ) ↦
    1 / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ε (b i * (↑n : ℝ)) - ε (↑n : ℝ)) 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]

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, Real.log, Filter.atTop, AkraBazziRecurrence.smoothingFn, HPow.hPow, AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self, Asymptotics.IsEquivalent.isTheta, OfNat.ofNat, Neg.neg
-- 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 : α
h : Membership.mem (γ := Finset α) univ i
⊢ Continuous (Y := ℝ) fun (p : ℝ) ↦ a i

Tactic:
fun_prop
-- 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 : ∀ (i : α), Membership.mem (γ := Finset α) univ i → Continuous (X := ℝ) (HPow.hPow (b i))
⊢ Continuous (Y := ℝ) fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p

Tactic:
refine continuous_finsetSum Finset.univ fun i _ => Continuous.mul (by fun_prop) ?_

Premises used: Finset.univ, Continuous.mul, continuous_finsetSum
-- 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 : α
h : Membership.mem (γ := Finset α) univ i
⊢ Continuous (X := ℝ) (HPow.hPow (b i))

Tactic:
Continuous.rpow continuous_const continuous_id (fun x => Or.inl (ne_of_gt (R.b_pos i)))

Premises used: continuous_const, Continuous.rpow, ne_of_gt, continuous_id, AkraBazziRecurrence.b_pos, Or.inl
-- 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 : α
h : Membership.mem (γ := Finset α) univ i
⊢ Continuous (X := ℝ) (HPow.hPow (b i))

Tactic:
exact Continuous.rpow continuous_const continuous_id (fun x => Or.inl (ne_of_gt (R.b_pos i)))

Premises used: continuous_const, Continuous.rpow, ne_of_gt, continuous_id, AkraBazziRecurrence.b_pos, Or.inl
-- 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 : StrictAnti (α := ℝ) (β := ℝ) (∑ c : α, fun (p : ℝ) ↦ a c * b c ^ p)
⊢ StrictAnti (β := ℝ) fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p

Tactic:
rw [← Finset.sum_fn]

Premises used: Finset.sum_fn
-- 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
⊢ StrictAnti (α := ℝ) (β := ℝ) (∑ c : α, fun (p : ℝ) ↦ a c * b c ^ p)

Tactic:
Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms

Premises used: Finset.sum_induction_nonempty, Finset.univ_nonempty, StrictAnti.add
-- 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
terms : ∀ (x : α), Membership.mem (γ := Finset α) univ x → StrictAnti (β := ℝ) fun (p : ℝ) ↦ a x * b x ^ p
⊢ StrictAnti (α := ℝ) (β := ℝ) (∑ c : α, fun (p : ℝ) ↦ a c * b c ^ p)

Tactic:
refine Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms
-- 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
⊢ ∀ (x : α), Membership.mem (γ := Finset α) univ x → StrictAnti (β := ℝ) fun (p : ℝ) ↦ a x * b x ^ p

Tactic:
fun i _ => StrictAnti.const_mul ?_ (R.a_pos i)

Premises used: StrictAnti.const_mul, AkraBazziRecurrence.a_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
terms : ∀ (i : α), Membership.mem (γ := Finset α) univ i → StrictAnti (α := ℝ) (HPow.hPow (b i))
⊢ ∀ (x : α), Membership.mem (γ := Finset α) univ x → StrictAnti (β := ℝ) fun (p : ℝ) ↦ a x * b x ^ p

Tactic:
refine fun i _ => StrictAnti.const_mul ?_ (R.a_pos i)

Premises used: StrictAnti.const_mul, AkraBazziRecurrence.a_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
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ StrictAnti (α := ℝ) (HPow.hPow (b i))

Tactic:
Real.strictAnti_rpow_of_base_lt_one (R.b_pos i) (R.b_lt_one i)

Premises used: Real.strictAnti_rpow_of_base_lt_one, AkraBazziRecurrence.b_pos, AkraBazziRecurrence.b_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
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ StrictAnti (α := ℝ) (HPow.hPow (b i))

Tactic:
exact Real.strictAnti_rpow_of_base_lt_one (R.b_pos i) (R.b_lt_one i)

Premises used: Real.strictAnti_rpow_of_base_lt_one, AkraBazziRecurrence.b_pos, AkraBazziRecurrence.b_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
⊢ Eq (α := ℝ) (∑ x : α, 0) 0

Tactic:
simp
-- 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 : α, 0) 0

Tactic:
have h₁ : Finset.univ.sum (fun _ : α => (0 : ℝ)) = 0 := by simp
-- 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₁ : Eq (α := ℝ) (∑ x : α, 0) 0
rw : Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 (∑ x : α, 0))
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 0)

Tactic:
rw [← h₁]
-- 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₁ : Eq (α := ℝ) (∑ x : α, 0) 0
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 (∑ x : α, 0))

Tactic:
tendsto_finsetSum (univ : Finset α) (fun i _ => ?_)

Premises used: Finset.univ, tendsto_finsetSum
-- 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₁ : Eq (α := ℝ) (∑ x : α, 0) 0
refine : ∀ (i : α), Membership.mem (γ := Finset α) univ i → Tendsto (β := ℝ) (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atTop (𝓝 (∑ x : α, 0))

Tactic:
refine tendsto_finsetSum (univ : Finset α) (fun i _ => ?_)

Premises used: Finset.univ, tendsto_finsetSum
-- 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₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
rw : Tendsto (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 (a i * 0))
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 0)

Tactic:
rw [← mul_zero (a i)]

Premises used: MulZeroClass.mul_zero
-- 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₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ Tendsto (fun (p : ℝ) ↦ a i) atTop (𝓝 (a i))

Tactic:
simp
-- 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₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
refine : -1 < b i
⊢ Tendsto (fun (p : ℝ) ↦ a i * b i ^ p) atTop (𝓝 (a i * 0))

Tactic:
refine Tendsto.mul (by simp) <| tendsto_rpow_atTop_of_base_lt_one _ ?_ (R.b_lt_one i)

Premises used: tendsto_rpow_atTop_of_base_lt_one, Filter.Tendsto.mul, AkraBazziRecurrence.b_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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ 0 < b i

Tactic:
have := R.b_pos 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
h₁ : Eq (α := ℝ) (∑ x : α, 0) 0
i : α
h : Membership.mem (γ := Finset α) univ i
this : 0 < b i
linarith : b i ≤ -1 → -1 + (0 - b i) + (b i - -1) = 0
⊢ -1 < b i

Tactic:
linarith
-- 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
⊢ 0 < b (max_bi b)

Tactic:
have := R.b_pos (max_bi b)
-- 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
this : 0 < b (max_bi b)
linarith : b (max_bi b) ≤ 0 → 0 - b (max_bi b) + (b (max_bi b) - 0) = 0
⊢ 0 < b (max_bi b)

Tactic:
linarith
-- 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
⊢ 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 _)
-- 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
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atBot atTop

Tactic:
tendsto_atTop_mono (fun p => ?_) h₁

Premises used: Filter.tendsto_atTop_mono
-- 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
refine : ∀ (p : ℝ), a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p
⊢ Tendsto (β := ℝ) (fun (p : ℝ) ↦ ∑ i : α, a i * b i ^ p) atBot atTop

Tactic:
refine tendsto_atTop_mono (fun p => ?_) h₁

Premises used: Filter.tendsto_atTop_mono
-- 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 : ℝ
⊢ a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p

Tactic:
Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)

Premises used: Finset.mem_univ, Finset.single_le_sum
-- 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 : ℝ
refine : ∀ (i : α), Membership.mem (γ := Finset α) univ i → LE.le (α := ℝ) 0 ((fun (i : α) ↦ a i * b i ^ p) i)
⊢ a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p

Tactic:
refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)

Premises used: Finset.mem_univ, Finset.single_le_sum