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
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo :
  ∀ ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : ℕ) in atTop, ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ c * Norm.norm (E := ℝ) (↑x : ℝ)
hlo' :
  ∀ᶠ (x : ℕ) in atTop,
    ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ (1 - b (max_bi b)) / 2 * Norm.norm (E := ℝ) (↑x : ℝ)
n : ℕ
hn' : ∀ (i : α), (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
hn : (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (1 - b (max_bi b)) / 2 * (↑n : ℝ)
⊢ b i ≤ b (max_bi b)

Tactic:
max_bi_le _

Premises used: AkraBazziRecurrence.max_bi_le
-- 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 : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo :
  ∀ ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : ℕ) in atTop, ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ c * Norm.norm (E := ℝ) (↑x : ℝ)
hlo' :
  ∀ᶠ (x : ℕ) in atTop,
    ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ (1 - b (max_bi b)) / 2 * Norm.norm (E := ℝ) (↑x : ℝ)
n : ℕ
hn' : ∀ (i : α), (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
hn : (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (1 - b (max_bi b)) / 2 * (↑n : ℝ)
⊢ b i ≤ b (max_bi b)

Tactic:
exact max_bi_le _

Premises used: AkraBazziRecurrence.max_bi_le
-- 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 : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo :
  ∀ ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : ℕ) in atTop, ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ c * Norm.norm (E := ℝ) (↑x : ℝ)
hlo' :
  ∀ᶠ (x : ℕ) in atTop,
    ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ (1 - b (max_bi b)) / 2 * Norm.norm (E := ℝ) (↑x : ℝ)
n : ℕ
hn' : ∀ (i : α), (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
hn : (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (1 - b (max_bi b)) / 2 * (↑n : ℝ)
calc : (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
calc₁ :
  b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ b i * (↑n : ℝ) + (1 - b (max_bi b)) / 2 * (↑n : ℝ)
calc₂ : b i * (↑n : ℝ) + (1 - b (max_bi b)) / 2 * (↑n : ℝ) = (b i + (1 - b (max_bi b)) / 2) * (↑n : ℝ)
calc₃ : (b i + (1 - b (max_bi b)) / 2) * (↑n : ℝ) ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * (↑n : ℝ)
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)

Tactic:
calc r i n ≤ b i * n + n / log n ^ 2 := by exact hn' i
             _ ≤ b i * n + (1 - b (max_bi b)) / 2 * n := by gcongr
             _ = (b i + (1 - b (max_bi b)) / 2) * n := by ring
             _ ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * n := by gcongr; exact max_bi_le _

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast, Real.log, HAdd.hAdd, AkraBazziRecurrence.max_bi, 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
rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < r i x
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 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 < r i x

Tactic:
fun i => (R.tendsto_atTop_r i).eventually_gt_atTop 0

Premises used: AkraBazziRecurrence.tendsto_atTop_r, OfNat.ofNat, Filter.Tendsto.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
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < r i x

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually_gt_atTop 0

Premises used: AkraBazziRecurrence.tendsto_atTop_r, OfNat.ofNat, Filter.Tendsto.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 < log (b i * (↑x : ℝ))
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < log (b 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 : α
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ log (b i * (↑n : ℝ))) atTop atTop

Tactic:
have h : Tendsto (fun (n : ℕ) => log (b i * n)) atTop atTop :=
    Tendsto.comp tendsto_log_atTop
      <| Tendsto.const_mul_atTop (b_pos R i) tendsto_natCast_atTop_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 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ log (b i * (↑n : ℝ))) atTop atTop
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * (↑x : ℝ))

Tactic:
h.eventually_gt_atTop 0

Premises used: OfNat.ofNat, Filter.Tendsto.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
i : α
h : Tendsto (β := ℝ) (fun (n : ℕ) ↦ log (b i * (↑n : ℝ))) atTop atTop
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * (↑x : ℝ))

Tactic:
exact h.eventually_gt_atTop 0

Premises used: OfNat.ofNat, Filter.Tendsto.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
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : n < R.n₀
⊢ 0 < T n

Tactic:
R.T_gt_zero' n hn

Premises used: AkraBazziRecurrence.T_gt_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
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : n < R.n₀
⊢ 0 < T n

Tactic:
exact R.T_gt_zero' n hn

Premises used: AkraBazziRecurrence.T_gt_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
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
ind : 0 < ∑ i : α, a i * T (r i n) + g (↑n : ℝ)
⊢ 0 < T n

Tactic:
rw [R.h_rec n hn]

Premises used: AkraBazziRecurrence.h_rec
-- 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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ 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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 ≤ g (↑n : ℝ)

Tactic:
simp_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
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
sum_elems : ∀ (i : α), Membership.mem (γ := Finset α) univ i → 0 < a i * T (r i n)
⊢ 0 < ∑ i : α, a i * T (r i n) + g (↑n : ℝ)

Tactic:
refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by simp_all)

Premises used: Finset.sum_pos, Finset.univ_nonempty, add_pos_of_pos_of_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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ ∀ (i : α), Membership.mem (γ := Finset α) univ i → 0 < a i * T (r i n)

Tactic:
fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Premises used: AkraBazziRecurrence.r_lt_n, mul_pos, 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
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ ∀ (i : α), Membership.mem (γ := Finset α) univ i → 0 < a i * T (r i n)

Tactic:
exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Premises used: AkraBazziRecurrence.r_lt_n, mul_pos, 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
n : ℕ
h_ind : ∀ m < n, 0 < T m
⊢ n < R.n₀ ∨ R.n₀ ≤ n

Tactic:
cases lt_or_ge n R.n₀ with
    | inl hn => exact R.T_gt_zero' n hn -- n < R.n₀
    | inr hn => -- R.n₀ ≤ n
      rw [R.h_rec n hn]
      have := R.g_nonneg
      refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by simp_all)
      exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Premises used: AkraBazziRecurrence.n₀, lt_or_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
n : ℕ
ind : ∀ (n : ℕ) (h_ind : ∀ m < n, 0 < T m), 0 < T n
⊢ 0 < T n

Tactic:
induction n using Nat.strongRecOn with
  | ind n h_ind =>
    cases lt_or_ge n R.n₀ with
    | inl hn => exact R.T_gt_zero' n hn -- n < R.n₀
    | inr hn => -- R.n₀ ≤ n
      rw [R.h_rec n hn]
      have := R.g_nonneg
      refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by simp_all)
      exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Premises used: AkraBazziRecurrence.n₀, lt_or_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
n : ℕ
⊢ 0 ≤ T n

Tactic:
le_of_lt <| R.T_pos n

Premises used: AkraBazziRecurrence.T_pos, le_of_lt
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
simp : 1 + 1 / log x ≤ HAdd.hAdd (α := ℝ) 1 1
⊢ 1 + ε x ≤ 2

Tactic:
simp only [smoothingFn, ← one_add_one_eq_two]

Premises used: one_add_one_eq_two, AkraBazziRecurrence.smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
bc : 1 / log x ≤ 1
⊢ 1 + 1 / log x ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 = rexp 0

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ rexp 0 < rexp 1

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ rexp 1 ≤ x

Tactic:
hx
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
calc : 1 = rexp 0
calc₁ : rexp 0 < rexp 1
⊢ 1 < x

Tactic:
calc 1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx

Premises used: Real.exp, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 < x

Tactic:
have : 1 < x := by
    calc 1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
bc : 1 ≤ log x
⊢ 1 / log x ≤ 1

Tactic:
rw [div_le_one (log_pos this)]

Premises used: Real.log_pos, div_le_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 = log (rexp 1)

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ log (rexp 1) ≤ log x

Tactic:
log_le_log (exp_pos _) hx

Premises used: Real.log_le_log, Real.exp_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
calc : 1 = log (rexp 1)
⊢ 1 ≤ log x

Tactic:
calc 1 = log (exp 1) := by simp
       _ ≤ log x := log_le_log (exp_pos _) hx

Premises used: Real.exp, Real.log_le_log, Real.log, OfNat.ofNat, Real.exp_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℝ) ↦ 1 / log n) fun (x : ℝ) ↦ 1

Tactic:
isLittleO_of_tendsto (fun _ h => False.elim <| one_ne_zero h) ?_

Premises used: False.elim, Asymptotics.isLittleO_of_tendsto, one_ne_zero
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 / log x / 1) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℝ) ↦ 1 / log n) fun (x : ℝ) ↦ 1

Tactic:
refine isLittleO_of_tendsto (fun _ h => False.elim <| one_ne_zero h) ?_

Premises used: False.elim, Asymptotics.isLittleO_of_tendsto, one_ne_zero
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 / log x / 1) atTop (𝓝 0)

Tactic:
simp only [one_div, div_one]

Premises used: one_div, div_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) atTop (𝓝 0)

Tactic:
Tendsto.inv_tendsto_atTop Real.tendsto_log_atTop

Premises used: Real.tendsto_log_atTop, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) atTop (𝓝 0)

Tactic:
exact Tendsto.inv_tendsto_atTop Real.tendsto_log_atTop

Premises used: Real.tendsto_log_atTop, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsEquivalent (E' := ℝ) atTop (fun (x : ℝ) ↦ 1 + ε x) fun (x : ℝ) ↦ 1

Tactic:
IsEquivalent.add_isLittleO IsEquivalent.refl isLittleO_smoothingFn_one

Premises used: Asymptotics.IsEquivalent.add_isLittleO, Asymptotics.IsEquivalent.refl, AkraBazziRecurrence.isLittleO_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsEquivalent (E' := ℝ) atTop (fun (x : ℝ) ↦ 1 - ε x) fun (x : ℝ) ↦ 1

Tactic:
IsEquivalent.sub_isLittleO IsEquivalent.refl isLittleO_smoothingFn_one

Premises used: Asymptotics.IsEquivalent.sub_isLittleO, Asymptotics.IsEquivalent.refl, AkraBazziRecurrence.isLittleO_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ GrowsPolynomially fun (x : ℝ) ↦ 1 - ε x

Tactic:
GrowsPolynomially.of_isEquivalent_const isEquivalent_one_sub_smoothingFn_one

Premises used: AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent_const, AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ GrowsPolynomially fun (x : ℝ) ↦ 1 + ε x

Tactic:
GrowsPolynomially.of_isEquivalent_const isEquivalent_one_add_smoothingFn_one

Premises used: AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent_const, AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
rw : IsEquivalent (E' := ℝ) atTop (fun (x : ℝ) ↦ 1 - ε x) (Function.const ℝ 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - ε x) atTop (𝓝 1)

Tactic:
rw [← isEquivalent_const_iff_tendsto one_ne_zero]

Premises used: one_ne_zero, Asymptotics.isEquivalent_const_iff_tendsto
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
⊢ IsEquivalent (E' := ℝ) atTop (fun (x : ℝ) ↦ 1 - ε x) (Function.const ℝ 1)

Tactic:
isEquivalent_one_sub_smoothingFn_one

Premises used: AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
⊢ IsEquivalent (E' := ℝ) atTop (fun (x : ℝ) ↦ 1 - ε x) (Function.const ℝ 1)

Tactic:
exact isEquivalent_one_sub_smoothingFn_one

Premises used: AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - ε x) atTop (𝓝 1)

Tactic:
have h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1) := by
    rw [← isEquivalent_const_iff_tendsto one_ne_zero]
    exact isEquivalent_one_sub_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
h₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - ε x) atTop (𝓝 1)
⊢ (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'

Tactic:
rw [tendsto_order] at h₁

Premises used: tendsto_order
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
h₁ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
h₁.1 c hc

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
h₁ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
exact h₁.1 c hc

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
c : ℝ
hc : c < 1
⊢ ∀ᶠ (n : ℕ) in atTop, c < 1 - ε (↑n : ℝ)

Tactic:
Eventually.natCast_atTop (p := fun n => c < 1 - ε n)
    <| eventually_one_sub_smoothingFn_gt_const_real c hc

Premises used: AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const_real, Filter.Eventually.natCast_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < 1 - ε x

Tactic:
eventually_one_sub_smoothingFn_gt_const_real 0 zero_lt_one

Premises used: AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const_real, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 - ε (↑n : ℝ)

Tactic:
eventually_one_sub_smoothingFn_pos_real.natCast_atTop

Premises used: Filter.Eventually.natCast_atTop, AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos_real
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (n : ℕ) (hn : 0 < 1 - ε (↑n : ℝ)), 0 ≤ 1 - ε (↑n : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε (↑n : ℝ)

Tactic:
filter_upwards [eventually_one_sub_smoothingFn_pos] with n hn

Premises used: AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
n : ℕ
hn : 0 < 1 - ε (↑n : ℝ)
⊢ 0 ≤ 1 - ε (↑n : ℝ)

Tactic:
le_of_lt hn

Premises used: le_of_lt
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
n : ℕ
hn : 0 < 1 - ε (↑n : ℝ)
⊢ 0 ≤ 1 - ε (↑n : ℝ)

Tactic:
exact le_of_lt hn

Premises used: le_of_lt
-- 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 < 1 - ε (↑(r i x) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 - ε (↑(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 < 1 - ε (↑(r i x) : ℝ)

Tactic:
fun i => (R.tendsto_atTop_r_real i).eventually eventually_one_sub_smoothingFn_pos_real

Premises used: AkraBazziRecurrence.tendsto_atTop_r_real, AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos_real, 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 < 1 - ε (↑(r i x) : ℝ)

Tactic:
exact fun i => (R.tendsto_atTop_r_real i).eventually eventually_one_sub_smoothingFn_pos_real

Premises used: AkraBazziRecurrence.tendsto_atTop_r_real, AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos_real, Filter.Tendsto.eventually
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < x

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ log x ≠ 0

Tactic:
have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
this : log x ≠ 0
simp_rw : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ (log z)⁻¹) x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 / log z) x

Tactic:
simp_rw [one_div]

Premises used: one_div
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ x ≠ 0

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ (log z)⁻¹) x

Tactic:
exact DifferentiableAt.inv (differentiableAt_log (by positivity)) this

Premises used: Real.differentiableAt_log, DifferentiableAt.inv
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 - ε z) x

Tactic:
DifferentiableAt.sub (differentiableAt_const _) <| differentiableAt_smoothingFn hx

Premises used: DifferentiableAt.sub, AkraBazziRecurrence.differentiableAt_smoothingFn, differentiableAt_const
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ DifferentiableOn ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 - ε z) (Set.Ioi 1)

Tactic:
fun _ hx => (differentiableAt_one_sub_smoothingFn hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn, DifferentiableOn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 + ε z) x

Tactic:
DifferentiableAt.add (differentiableAt_const _) <| differentiableAt_smoothingFn hx

Premises used: AkraBazziRecurrence.differentiableAt_smoothingFn, differentiableAt_const, DifferentiableAt.add
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ DifferentiableOn ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 + ε z) (Set.Ioi 1)

Tactic:
fun _ hx => (differentiableAt_one_add_smoothingFn hx).differentiableWithinAt

Premises used: AkraBazziRecurrence.differentiableAt_one_add_smoothingFn, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
simp_rw : deriv (fun (n : ℝ) ↦ (log n)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv (fun (n : ℝ) ↦ 1 / log n) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
simp_rw [one_div]

Premises used: one_div
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
⊢ deriv (fun (n : ℝ) ↦ (log n)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
apply deriv_inv_log

Premises used: Real.deriv_inv_log
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (x : ℝ), deriv ε x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv ε =ᶠ[atTop] fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
filter_upwards with x
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
h h₁ : -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2 = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv ε x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
rw [deriv_smoothingFn]

Premises used: AkraBazziRecurrence.deriv_smoothingFn