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 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

Tactic:
exact (mul_div_cancel_left₀ _ (by positivity)).symm

Premises used: mul_div_cancel_left₀, Eq.symm
-- 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 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
hbc : C / c ≤ (↑⌈C / c⌉₊ : ℝ)
⊢ c * (C / c) ≤ c * (↑⌈C / c⌉₊ : ℝ)

Tactic:
gcongr
-- 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 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⌉₊ : ℝ)

Tactic:
simp [Nat.le_ceil]

Premises used: Nat.le_ceil
-- 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 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
ha : 0 ≤ c
⊢ c * (↑⌈C / c⌉₊ : ℝ) ≤ c * (↑n : ℝ)

Tactic:
gcongr
-- 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 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 * (↑n : ℝ) ≤ (↑(r i n) : ℝ)

Tactic:
hn₂ 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
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⌉₊ : ℝ)
calc₂ : c * (↑⌈C / c⌉₊ : ℝ) ≤ c * (↑n : ℝ)
⊢ C ≤ (↑(r i 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

Premises used: HDiv.hDiv
-- 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 : ∀ (b : ℕ), ∀ᶠ (a : ℕ) in atTop, b ≤ r i a
⊢ Tendsto (r i) atTop atTop

Tactic:
rw [tendsto_atTop]

Premises used: Filter.tendsto_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), LE.le (α := ℝ) (↑b : ℝ) (↑(r i n) : ℝ)

Tactic:
have := R.eventually_r_ge b
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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) : ℝ)
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, LE.le (α := ℝ) (↑b : ℝ) (↑(r i x) : ℝ)

Tactic:
rw [Filter.eventually_all] at this

Premises used: Filter.eventually_all
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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 : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, LE.le (α := ℝ) (↑b : ℝ) (↑(r i x) : ℝ)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Tactic:
exact_mod_cast this 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 : α
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑(r i n) : ℝ)) atTop atTop

Tactic:
Tendsto.comp tendsto_natCast_atTop_atTop (R.tendsto_atTop_r i)

Premises used: AkraBazziRecurrence.tendsto_atTop_r, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- 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
⊢ 0 < b (max_bi b)

Tactic:
have h_max_bi_pos : 0 < b (max_bi b) := R.b_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
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
⊢ b (max_bi b) < 1

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

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
-- 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)
⊢ 0 < c

Tactic:
positivity
-- 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)
⊢ 0 < c

Tactic:
have hc_pos : 0 < c := by positivity
-- 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
⊢ 0 < (1 - b (max_bi b)) / 2

Tactic:
positivity
-- 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
⊢ 0 < (1 - b (max_bi b)) / 2

Tactic:
have h₁ : 0 < (1 - b (max_bi b)) / 2 := by positivity
-- 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
⊢ b (max_bi b) + (1 - b (max_bi b)) / 2 = b (max_bi b) * (1 / 2) + 1 / 2

Tactic:
ring
-- 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
bc : b (max_bi b) < 1
⊢ b (max_bi b) * (1 / 2) + 1 / 2 < 1 * (1 / 2) + 1 / 2

Tactic:
gcongr
-- 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
⊢ b (max_bi b) < 1

Tactic:
R.b_lt_one _

Premises used: 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
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

Tactic:
exact R.b_lt_one _

Premises used: 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
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
⊢ 1 * (1 / 2) + 1 / 2 = 1

Tactic:
norm_num
-- 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
⊢ 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
-- 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
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)

Tactic:
⟨c, ⟨hc_pos, hc_lt_one⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)

Tactic:
refine ⟨c, ⟨hc_pos, hc_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
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
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)

Tactic:
have hlo := isLittleO_self_div_log_id
-- 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 :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)
⊢ ∀ ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : ℕ) in atTop, ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ c * Norm.norm (E := ℝ) (↑x : ℝ)

Tactic:
rw [Asymptotics.isLittleO_iff] at hlo

Premises used: Asymptotics.isLittleO_iff
-- 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 : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖(↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2‖ ≤ (1 - b (max_bi b)) / 2 * Norm.norm (E := ℝ) (↑x : ℝ)

Tactic:
have hlo' := hlo 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
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 : ℝ)
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 : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)

Tactic:
filter_upwards [hlo', R.eventually_r_le_b] with n hn hn'

Premises used: AkraBazziRecurrence.eventually_r_le_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
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 : α
⊢ 0 ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
positivity
-- 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 : ‖(↑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 : α
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 : ℝ)
⊢ (↑(r i n) : ℝ) ≤ c * (↑n : ℝ)

Tactic:
rw [Real.norm_of_nonneg (by positivity)] at hn

Premises used: Real.norm_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
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 : α
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- 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 : (↑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 : α
⊢ (↑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

Premises used: Real.norm_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
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) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
hn' 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
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) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
exact hn' 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
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 * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ b i * (↑n : ℝ) + (1 - b (max_bi b)) / 2 * (↑n : ℝ)

Tactic:
gcongr
-- 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 * (↑n : ℝ) + (1 - b (max_bi b)) / 2 * (↑n : ℝ) = (b i + (1 - b (max_bi b)) / 2) * (↑n : ℝ)

Tactic:
ring
-- 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 : ℝ)
hbc : b i ≤ b (max_bi b)
⊢ (b i + (1 - b (max_bi b)) / 2) * (↑n : ℝ) ≤ (b (max_bi b) + (1 - b (max_bi b)) / 2) * (↑n : ℝ)

Tactic:
gcongr