awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := 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 : (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (1 - b (max_bi b)) / 2 * Norm.norm (E := ℝ) (↑n : ℝ)
hn' : ∀ (i : α), (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have hn₁ : (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (1 - b (max_bi b)) / 2 * (↑n : ℝ)
Tactic: simp only [Real.norm_of_nonneg (by positivity : 0 ≤ (n : ℝ))] at hn
Cleared hypotheses: 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
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 + (1 - b (max_bi b)) / 2) * (↑n : ℝ) ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * (↑n : ℝ)
have hbc : b i ≤ b (max_bi b)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := 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 : ℝ)
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have calc : (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
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 _
-- 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 : ℝ := 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
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have calc₁ : b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ b i * (↑n : ℝ) + (1 - b (max_bi b)) / 2 * (↑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 _
-- 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 : ℝ := 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 : ℝ)
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have calc₂ : b i * (↑n : ℝ) + (1 - b (max_bi b)) / 2 * (↑n : ℝ) = (b i + (1 - b (max_bi b)) / 2) * (↑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 _
-- 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 : ℝ := 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 : ℝ)
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have calc₃ : (b i + (1 - b (max_bi b)) / 2) * (↑n : ℝ) ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * (↑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 _
-- 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 < r i n
have rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < log (b i * (↑n : ℝ))
have rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * (↑x : ℝ))
Tactic: rw [Filter.eventually_all]
-- 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 : α
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * (↑x : ℝ))
have h : 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
-- 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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < T n
have ind : 0 < ∑ i : α, a i * T (r i n) + g (↑n : ℝ)
Tactic: rw [R.h_rec n hn]
-- 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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < ∑ i : α, a i * T (r i n) + g (↑n : ℝ)
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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 < ∑ i : α, a i * T (r i n) + g (↑n : ℝ)
have sum_elems : ∀ (i : α), Membership.mem (γ := Finset α) univ i → 0 < a i * T (r i n)
Tactic: refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by simp_all)
-- 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 : ℕ
h_ind : ∀ m < n, 0 < T m
⊢ 0 < T n
have x : 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)
-- 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 : ℕ
⊢ 0 < T n
have ind : ∀ (n : ℕ) (h_ind : ∀ m < n, 0 < T m), 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)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 + ε x ≤ 2
have simp : 1 + 1 / log x ≤ HAdd.hAdd (α := ℝ) 1 1
Tactic: simp only [smoothingFn, ← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 + 1 / log x ≤ HAdd.hAdd (α := ℝ) 1 1
have bc : 1 / log x ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 < x
have calc : 1 = rexp 0
Tactic: calc 1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : rexp 1 ≤ x
calc : 1 = rexp 0
⊢ 1 < x
have calc₁ : rexp 0 < rexp 1
Tactic: calc 1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
x : ℝ
hx : rexp 1 ≤ x
⊢ 1 / log x ≤ 1
have this : 1 < x
Tactic: have : 1 < x := by
    calc 1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 / log x ≤ 1
have bc : 1 ≤ log x
Tactic: rw [div_le_one (log_pos this)]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 ≤ log x
have calc : 1 = log (rexp 1)
Tactic: calc 1 = log (exp 1) := by simp
       _ ≤ log x := log_le_log (exp_pos _) hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℝ) ↦ 1 / log n) fun (x : ℝ) ↦ 1
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 / log x / 1) atTop (𝓝 0)
Tactic: refine isLittleO_of_tendsto (fun _ h => False.elim <| one_ne_zero h) ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 / log x / 1) atTop (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) atTop (𝓝 0)
Tactic: simp only [one_div, div_one]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
c : ℝ
hc : c < 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - ε x) atTop (𝓝 1)
have rw : IsEquivalent (E' := ℝ) atTop (fun (x : ℝ) ↦ 1 - ε x) (Function.const ℝ 1)
Tactic: rw [← isEquivalent_const_iff_tendsto one_ne_zero]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
c : ℝ
hc : c < 1
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x
have h₁ : 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
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
c : ℝ
hc : c < 1
h₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ 1 - ε x) atTop (𝓝 1)
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x
have h₂ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'
Tactic: rw [tendsto_order] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε (↑n : ℝ)
have h : ∀ (n : ℕ) (hn : 0 < 1 - ε (↑n : ℝ)), 0 ≤ 1 - ε (↑n : ℝ)
Tactic: filter_upwards [eventually_one_sub_smoothingFn_pos] with 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 < 1 - ε (↑(r i n) : ℝ)
have rw : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 - ε (↑(r i x) : ℝ)
Tactic: rw [Filter.eventually_all]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x
have this : log x ≠ 0
Tactic: have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 / log z) x
have simp_rw : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ (log z)⁻¹) x
Tactic: simp_rw [one_div]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
⊢ deriv (fun (n : ℝ) ↦ 1 / log n) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have simp_rw : deriv (fun (n : ℝ) ↦ (log n)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: simp_rw [one_div]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ deriv ε =ᶠ[atTop] fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have h : ∀ (x : ℝ), deriv ε x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
⊢ deriv ε x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have h : -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2 = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: rw [deriv_smoothingFn]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
have simp_rw : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)) fun (x : ℝ) ↦
  (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
Tactic: simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
simp_rw :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
have simp_rw₁ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ * (HPow.hPow (β := ℕ) (log x) 2)⁻¹)) fun (x : ℝ) ↦
  (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
Tactic: simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
simp_rw :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
simp_rw₁ :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ * (HPow.hPow (β := ℕ) (log x) 2)⁻¹)) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
have simp_rw₂ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x * HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (x : ℝ) ↦
  (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
Tactic: simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
simp_rw :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
simp_rw₁ :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x⁻¹ * (HPow.hPow (β := ℕ) (log x) 2)⁻¹)) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
simp_rw₂ :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -(x * HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
have simp_rw₃ : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ (-(x * HPow.hPow (β := ℕ) (log x) 2))⁻¹) fun (x : ℝ) ↦
  (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹
Tactic: simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (x : ℝ) ↦ (x * 1)⁻¹
have refine_1 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x * 1) fun (x : ℝ) ↦ -x * HPow.hPow (β := ℕ) (log x) 2
Tactic: refine IsLittleO.inv_rev ?_ ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
refine_1 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x * 1) fun (x : ℝ) ↦ -x * HPow.hPow (β := ℕ) (log x) 2
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (x : ℝ) ↦ (x * 1)⁻¹
have refine_2 : ∀ᶠ (x : ℝ) in atTop, x * 1 = 0 → -x * HPow.hPow (β := ℕ) (log x) 2 = 0
Tactic: refine IsLittleO.inv_rev ?_ ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ x) Neg.neg
have rw : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x) fun (x : ℝ) ↦ x
Tactic: rw [isBigO_neg_right]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x * 1) fun (x : ℝ) ↦ -x * HPow.hPow (β := ℕ) (log x) 2
have refine_1 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2
Tactic: refine IsBigO.mul_isLittleO
          (by rw [isBigO_neg_right]; aesop (add safe isBigO_refl)) ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2
have refine_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖HPow.hPow (β := ℕ) (log x) 2‖) atTop atTop
Tactic: rw [isLittleO_one_left_iff]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
x : ℝ
hx : x * 1 = 0
⊢ -x * HPow.hPow (β := ℕ) (log x) 2 = 0
have hx₁ : x = 0
Tactic: rw [mul_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ (deriv fun (x : ℝ) ↦ 1 - ε x) =ᶠ[atTop] -deriv ε
have h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 - ε x) x = (-deriv ε) x
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = (-deriv ε) x
have h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = (-deriv ε) x
Tactic: rw [deriv_fun_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = (-deriv ε) x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = (-deriv ε) x
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
Tactic: rw [deriv_fun_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = (-deriv ε) x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = (-deriv ε) x
have h₂ : DifferentiableAt ℝ ε x
Tactic: rw [deriv_fun_sub]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ -deriv ε =ᶠ[atTop] fun (x : ℝ) ↦ x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have h : ∀ (x : ℝ), (-deriv ε) x = x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ (deriv fun (x : ℝ) ↦ 1 + ε x) =ᶠ[atTop] deriv ε
have h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
have h : deriv (fun (x : ℝ) ↦ 1) x + deriv ε x = deriv ε x
Tactic: rw [deriv_fun_add]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x + deriv ε x = deriv ε x
⊢ deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
Tactic: rw [deriv_fun_add]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x + deriv ε x = deriv ε x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
⊢ deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
have h₂ : DifferentiableAt ℝ ε x
Tactic: rw [deriv_fun_add]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (x : ℝ) ↦ 1 - ε x) fun (z : ℝ) ↦ -deriv ε z
have h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 - ε x) x = -deriv ε x
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = -deriv ε x
have h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = -deriv ε x
Tactic: rw [deriv_fun_sub]