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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
h₁ : 0 ≤ b i
⊢ b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)
have h : b i * (↑n : ℝ) - (↑(r i n) : ℝ) ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: rw [sub_le_iff_le_add, add_comm, ← sub_le_iff_le_add]
-- 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 : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
h₁ : 0 ≤ b i
⊢ b i * (↑n : ℝ) - (↑(r i n) : ℝ) ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc : b i * (↑n : ℝ) - (↑(r i n) : ℝ) = ‖b i * (↑n : ℝ)‖ - Norm.norm (E := ℝ) (↑(r i n) : ℝ)
Tactic: calc (b i : ℝ) * n - r i n
    _ = ‖b i * n‖ - ‖(r i n : ℝ)‖ := by
      simp only [norm_mul, RCLike.norm_natCast, Real.norm_of_nonneg h₁]
    _ ≤ ‖(b i * n : ℝ) - r i n‖ := norm_sub_norm_le _ _
    _ = ‖(r i n : ℝ) - b i * n‖ := norm_sub_rev _ _
    _ ≤ n / log n ^ 2 := hn 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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have h : ∀ (n : ℕ) (hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) (i : α),
  (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: filter_upwards [R.dist_r_b'] with n hn 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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ)) ≤ b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖
have bc : (↑(r i n) : ℝ) - b i * (↑n : ℝ) ≤ ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖
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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have bc : ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc : (↑(r i n) : ℝ) = b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ))
Tactic: calc r i n = b i * n + (r i n - b i * n) := by ring
             _ ≤ b i * n + ‖r i n - b i * n‖ := by gcongr; exact Real.le_norm_self _
             _ ≤ b i * n + n / log n ^ 2 := by gcongr; exact hn 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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
calc : (↑(r i n) : ℝ) = b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ))
⊢ (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₁ : b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ)) ≤ b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖
Tactic: calc r i n = b i * n + (r i n - b i * n) := by ring
             _ ≤ b i * n + ‖r i n - b i * n‖ := by gcongr; exact Real.le_norm_self _
             _ ≤ b i * n + n / log n ^ 2 := by gcongr; exact hn 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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
calc : (↑(r i n) : ℝ) = b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ))
calc₁ : b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ)) ≤ b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖
⊢ (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
have calc₂ : b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
Tactic: calc r i n = b i * n + (r i n - b i * n) := by ring
             _ ≤ b i * n + ‖r i n - b i * n‖ := by gcongr; exact Real.le_norm_self _
             _ ≤ b i * n + n / log n ^ 2 := by gcongr; exact hn 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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), r i n < n
have h : ∀ (a_1 : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ R.n₀ ≤ x) x} x →
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ ∀ (i : α), r i n < n) x} x}
    a_1
Tactic: filter_upwards [eventually_ge_atTop R.n₀] with n hn i using R.r_lt_n i 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 : ℕ) ↦ R.n₀ ≤ x) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ ∀ (i : α), r i n < n) x} x}
      a_1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), r i n < n
have h₁ : ∀ (a_1 : ℕ), R.n₀ ≤ a_1 → ∀ (i : α), r i a_1 < a_1
Tactic: filter_upwards [eventually_ge_atTop R.n₀] with n hn i using R.r_lt_n i 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
⊢ b (min_bi b) / 2 < 1
have gt_zero : 0 < b (min_bi b)
Tactic: have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
-- 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
gt_zero : 0 < b (min_bi b)
⊢ b (min_bi b) / 2 < 1
have calc : b (min_bi b) / 2 < b (min_bi b)
Tactic: calc b (min_bi b) / 2
    _ < b (min_bi b) := by aesop (add safe apply div_two_lt_of_pos)
    _ < 1 := R.b_lt_one _
-- 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 : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
have gt_zero : 0 < b (min_bi b)
Tactic: have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
-- 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 : ℝ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ (↑(r i n) : ℝ)
have obtain : ∀ (c : ℝ) (hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c)
  (hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)),
  ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ (↑(r i 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 c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ (↑(r i n) : ℝ)
have h : ∀ (n : ℕ) (hn₁ : ⌈C / c⌉₊ ≤ n) (hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)) (i : α), C ≤ (↑(r i n) : ℝ)
Tactic: filter_upwards [eventually_ge_atTop ⌈C / c⌉₊, hc] with n hn₁ hn₂ 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
C c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
⊢ C ≤ (↑(r i n) : ℝ)
have h₁ : 0 < c
Tactic: have h₁ := hc_mem.1
-- 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 c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
h₁ : 0 < c
⊢ C = c * (C / c)
have rw : C = c * C / c
Tactic: rw [← mul_div_assoc]
-- 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 c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
h₁ : 0 < c
⊢ c * (C / c) ≤ c * (↑⌈C / c⌉₊ : ℝ)
have hbc : C / c ≤ (↑⌈C / c⌉₊ : ℝ)
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 c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
h₁ : 0 < c
⊢ c * (↑⌈C / c⌉₊ : ℝ) ≤ c * (↑n : ℝ)
have ha : 0 ≤ c
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 c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
h₁ : 0 < c
⊢ C ≤ (↑(r i n) : ℝ)
have calc : C = c * (C / c)
Tactic: calc C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ 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
C c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
h₁ : 0 < c
calc : C = c * (C / c)
⊢ C ≤ (↑(r i n) : ℝ)
have calc₁ : c * (C / c) ≤ c * (↑⌈C / c⌉₊ : ℝ)
Tactic: calc C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ 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
C c : ℝ
hc_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)
i : α
h₁ : 0 < c
calc : C = c * (C / c)
calc₁ : c * (C / c) ≤ c * (↑⌈C / c⌉₊ : ℝ)
⊢ C ≤ (↑(r i n) : ℝ)
have calc₂ : c * (↑⌈C / c⌉₊ : ℝ) ≤ c * (↑n : ℝ)
Tactic: calc C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ 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 : α
⊢ Tendsto (r i) atTop atTop
have rw : ∀ (b : ℕ), ∀ᶠ (a : ℕ) in atTop, b ≤ r i a
Tactic: rw [tendsto_atTop]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b_1 : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b_1 r
i : α
b : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a
have this : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), LE.le (α := ℝ) (↑b : ℝ) (↑(r i n) : ℝ)
Tactic: have := R.eventually_r_ge b
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.SumTransform (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b_1 : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b_1 r
i : α
b : ℕ
this : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), LE.le (α := ℝ) (↑b : ℝ) (↑(r i n) : ℝ)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a
have this₁ : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, LE.le (α := ℝ) (↑b : ℝ) (↑(r i x) : ℝ)
Tactic: rw [Filter.eventually_all] at this
Cleared hypotheses: this
-- 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
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have h_max_bi_pos : 0 < b (max_bi b)
Tactic: have h_max_bi_pos : 0 < b (max_bi b) := R.b_pos _
-- 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)
⊢ 0 < 1 - b (max_bi b)
have this : b (max_bi b) < 1
Tactic: have : b (max_bi b) < 1 := 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
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
this : b (max_bi b) < 1
⊢ 0 < 1 - b (max_bi b)
have linarith : 1 - b (max_bi b) ≤ 0 → b (max_bi b) - 1 + (1 - 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
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have h_max_bi_lt_one : 0 < 1 - b (max_bi b)
Tactic: have h_max_bi_lt_one : 0 < 1 - b (max_bi b) := by
    have : b (max_bi b) < 1 := R.b_lt_one _
    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
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)
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have hc_pos : 0 < c
Tactic: have hc_pos : 0 < c := by positivity
-- 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
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have h₁ : 0 < (1 - b (max_bi b)) / 2
Tactic: have h₁ : 0 < (1 - b (max_bi b)) / 2 := by positivity
-- 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
⊢ b (max_bi b) * (1 / 2) + 1 / 2 < 1 * (1 / 2) + 1 / 2
have bc : b (max_bi b) < 1
Tactic: gcongr
-- 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
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have hc_lt_one : c < 1
Tactic: have hc_lt_one : c < 1 :=
    calc b (max_bi b) + (1 - b (max_bi b)) / 2
      _ = b (max_bi b) * (1 / 2) + 1 / 2 := by ring
      _ < 1 * (1 / 2) + 1 / 2 := by gcongr; exact R.b_lt_one _
      _ = 1 := by norm_num
-- 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
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have refine : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
Tactic: refine ⟨c, ⟨hc_pos, hc_lt_one⟩, ?_⟩
-- 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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have hlo : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦ (↑n : ℝ)
Tactic: have hlo := isLittleO_self_div_log_id
-- 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 :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have hlo₁ : ∀ ⦃c : ℝ⦄,
  0 < c → ∀ᶠ (x : ℕ) in atTop, ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ c * Norm.norm (E := ℝ) (↑x : ℝ)
Tactic: rw [Asymptotics.isLittleO_iff] at hlo
Cleared hypotheses: hlo
-- 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 : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have hlo' : ∀ᶠ (x : ℕ) in atTop,
  ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ (1 - b (max_bi b)) / 2 * Norm.norm (E := ℝ) (↑x : ℝ)
Tactic: have hlo' := hlo 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
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 : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
have h : ∀ (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 : ℝ)
Tactic: filter_upwards [hlo', R.eventually_r_le_b] with n hn 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 : ‖(↑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 h : ∀ (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 : ℝ)
Tactic: rw [Real.norm_of_nonneg (by positivity)] at hn
Cleared hypotheses: hn, hn', i