awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg_1 : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun (x : ℝ) ↦ ‖g x‖) x) (c₄ * (fun (x : ℝ) ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound_1 : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
case : f u ≤ c₂ * ‖g u‖
case₁ : c₂ * ‖g u‖ ≤ c₂ * (c₄ * ‖g x‖)
case₂ : c₂ * (c₄ * ‖g x‖) = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖
case₃ : c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖)
case₄ : c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) ≤ c₂ * c₄ * c₁⁻¹ * f x
⊢ f u ≤ c₂ * c₄ * c₁⁻¹ * f x

Tactic:
case ub => calc
    f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
      _ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
      _ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
      _ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
      _ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
                gcongr
                rw [← Real.norm_of_nonneg (hf_pos x hbx)]
                exact h_lb x hbx

Premises used: Norm.norm, HMul.hMul, Inv.inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
h : ∀ (x : ℝ), f x = (g + (f - g)) x
⊢ f = g + (f - g)

Tactic:
ext
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
x : ℝ
⊢ f x = (g + (f - g)) x

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ f = g + (f - g)

Tactic:
have : f = g + (f - g) := by ext; simp
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
rw : GrowsPolynomially (g + (f - g))
⊢ GrowsPolynomially f

Tactic:
rw [this]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))

Tactic:
add_isLittleO hg hf

Premises used: AkraBazziRecurrence.GrowsPolynomially.add_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))

Tactic:
exact add_isLittleO hg hf

Premises used: AkraBazziRecurrence.GrowsPolynomially.add_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
c : ℝ
hf : f ~[atTop] fun (x : ℝ) ↦ c
⊢ GrowsPolynomially f

Tactic:
of_isEquivalent growsPolynomially_const hf

Premises used: AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent, AkraBazziRecurrence.growsPolynomially_const
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Finite α
inst_1 : Nonempty α
b : α → ℝ
i : α
⊢ b (min_bi b) ≤ b i

Tactic:
Classical.choose_spec (Finite.exists_min b) i

Premises used: Classical.choose_spec, Finite.exists_min, AkraBazziRecurrence.min_bi
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Finite α
inst_1 : Nonempty α
b : α → ℝ
i : α
⊢ b i ≤ b (max_bi b)

Tactic:
Classical.choose_spec (Finite.exists_max b) i

Premises used: Finite.exists_max, Classical.choose_spec, AkraBazziRecurrence.max_bi
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹

Tactic:
IsBigO.mul_isLittleO (isBigO_refl _ _) ?_

Premises used: Asymptotics.IsBigO.mul_isLittleO, Asymptotics.isBigO_refl
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦ 1⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_

Premises used: Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ ∀ᶠ (x : ℕ) in atTop, Eq (α := ℝ) 1 0 → HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2 = 0

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦ 1⁻¹

Tactic:
refine IsLittleO.inv_rev ?_ (by simp)

Premises used: Asymptotics.IsLittleO.inv_rev
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ 1) fun (x : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ LT.lt (α := ℕ) 0 2

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
_ : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ 1) fun (x : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 1) fun (n : ℕ) ↦ HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)

Premises used: Asymptotics.IsLittleO.pow, Nat.cast, Real.log, Real.isLittleO_const_log_atTop, Filter.atTop, HPow.hPow, Asymptotics.IsLittleO.natCast_atTop, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (x : ℕ), HMul.hMul (α := ℝ) (↑x : ℝ) 1⁻¹ = (↑x : ℝ)
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹) fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
ext
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℕ
⊢ HMul.hMul (α := ℝ) (↑x : ℝ) 1⁻¹ = (↑x : ℝ)

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
calc :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹
calc₁ :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) * (HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)⁻¹) fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹
calc₂ : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) 1⁻¹) fun (n : ℕ) ↦ (↑n : ℝ)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2) fun (n : ℕ) ↦
    (↑n : ℝ)

Tactic:
calc (fun (n : ℕ) => (n : ℝ) / log n ^ 2)
    _ = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by simp_rw [div_eq_mul_inv]
    _ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ := by
      refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
      refine IsLittleO.inv_rev ?_ (by simp)
      calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
    _ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, Real.log, Filter.atTop, Inv.inv, HPow.hPow, 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, ‖(↑(r i x) : ℝ) - b i * (↑x : ℝ)‖ ≤ (↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

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, ‖(↑(r i x) : ℝ) - b i * (↑x : ℝ)‖ ≤ (↑x : ℝ) / HPow.hPow (β := ℕ) (log (↑x : ℝ)) 2

Tactic:
simpa using IsLittleO.eventuallyLE (R.dist_r_b i)

Premises used: AkraBazziRecurrence.dist_r_b, Asymptotics.IsLittleO.eventuallyLE
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
h :
  ∀ (n : ℕ) (hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2)
    (i : α), b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)

Tactic:
filter_upwards [R.dist_r_b'] with n hn i

Premises used: AkraBazziRecurrence.dist_r_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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ 0 ≤ b i

Tactic:
have h₁ : 0 ≤ b i := le_of_lt <| 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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
h₁ : 0 ≤ b i
h : b i * (↑n : ℝ) - (↑(r i n) : ℝ) ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ b i * (↑n : ℝ) - (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2 ≤ (↑(r i n) : ℝ)

Tactic:
rw [sub_le_iff_le_add, add_comm, ← sub_le_iff_le_add]

Premises used: sub_le_iff_le_add, add_comm
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
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) : ℝ) = ‖b i * (↑n : ℝ)‖ - Norm.norm (E := ℝ) (↑(r i n) : ℝ)

Tactic:
simp only [norm_mul, RCLike.norm_natCast, Real.norm_of_nonneg h₁]

Premises used: norm_mul, RCLike.norm_natCast, 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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
h₁ : 0 ≤ b i
⊢ ‖b i * (↑n : ℝ)‖ - Norm.norm (E := ℝ) (↑(r i n) : ℝ) ≤ ‖b i * (↑n : ℝ) - (↑(r i n) : ℝ)‖

Tactic:
norm_sub_norm_le _ _

Premises used: norm_sub_norm_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
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) : ℝ)‖ = ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖

Tactic:
norm_sub_rev _ _

Premises used: norm_sub_rev
-- 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 : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
h₁ : 0 ≤ b i
⊢ ‖(↑(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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
h₁ : 0 ≤ b i
calc : b i * (↑n : ℝ) - (↑(r i n) : ℝ) = ‖b i * (↑n : ℝ)‖ - Norm.norm (E := ℝ) (↑(r i n) : ℝ)
⊢ b i * (↑n : ℝ) - (↑(r i n) : ℝ) ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

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

Premises used: HMul.hMul, Nat.cast, Real.log, norm_sub_norm_le, norm_sub_rev
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
h :
  ∀ (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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), (↑(r i n) : ℝ) ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2

Tactic:
filter_upwards [R.dist_r_b'] with n hn i

Premises used: AkraBazziRecurrence.dist_r_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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ (↑(r i n) : ℝ) = b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
bc : (↑(r i n) : ℝ) - b i * (↑n : ℝ) ≤ ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖
⊢ b i * (↑n : ℝ) + ((↑(r i n) : ℝ) - b i * (↑n : ℝ)) ≤ b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑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
n : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ (↑(r i n) : ℝ) - b i * (↑n : ℝ) ≤ ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖

Tactic:
Real.le_norm_self _

Premises used: Real.le_norm_self
-- 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 : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
⊢ (↑(r i n) : ℝ) - b i * (↑n : ℝ) ≤ ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖

Tactic:
exact Real.le_norm_self _

Premises used: Real.le_norm_self
-- 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 : ℕ
hn : ∀ (i : α), ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
i : α
bc : ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 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
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:
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
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:
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
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 : ℝ)‖
calc₂ :
  b i * (↑n : ℝ) + ‖(↑(r i n) : ℝ) - b i * (↑n : ℝ)‖ ≤ b i * (↑n : ℝ) + (↑n : ℝ) / HPow.hPow (β := ℕ) (log (↑n : ℝ)) 2
⊢ (↑(r 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

Premises used: HMul.hMul, HSub.hSub, Nat.cast, Real.log
-- 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 : ℕ
hn : R.n₀ ≤ n
i : α
⊢ r i n < n

Tactic:
R.r_lt_n i n hn

Premises used: AkraBazziRecurrence.r_lt_n
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
h :
  ∀ (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
h₁ h₂ : ∀ (n : ℕ) (hn : R.n₀ ≤ n) (i : α), r i n < n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), r i n < n

Tactic:
filter_upwards [eventually_ge_atTop R.n₀] with n hn i using R.r_lt_n i n hn

Premises used: AkraBazziRecurrence.n₀, Filter.eventually_ge_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
⊢ 0 < b (min_bi b)

Tactic:
have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ b (min_bi b) / 2 < b (min_bi b)

Tactic:
aesop (add safe apply div_two_lt_of_pos)

Premises used: div_two_lt_of_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
gt_zero : 0 < b (min_bi b)
⊢ b (min_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
gt_zero : 0 < b (min_bi b)
calc : b (min_bi b) / 2 < b (min_bi b)
⊢ b (min_bi b) / 2 < 1

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 _

Premises used: AkraBazziRecurrence.min_bi, 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
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ 0 < b (min_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
gt_zero : 0 < b (min_bi b)
⊢ ∃ (c : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c ∧ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)

Tactic:
exact ⟨b (min_bi b) / 2, ⟨⟨by positivity, R.bi_min_div_two_lt_one⟩, R.eventually_bi_mul_le_r⟩⟩
-- 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 : ℝ
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) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ (↑(r i n) : ℝ)

Tactic:
obtain ⟨c, hc_mem, hc⟩ := R.exists_eventually_const_mul_le_r

Premises used: AkraBazziRecurrence.exists_eventually_const_mul_le_r
-- 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) : ℝ)
h : ∀ (n : ℕ) (hn₁ : ⌈C / c⌉₊ ≤ n) (hn₂ : ∀ (i : α), c * (↑n : ℝ) ≤ (↑(r i n) : ℝ)) (i : α), C ≤ (↑(r i n) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ (↑(r i n) : ℝ)

Tactic:
filter_upwards [eventually_ge_atTop ⌈C / c⌉₊, hc] with n hn₁ hn₂ i

Premises used: HDiv.hDiv, Nat.ceil, Filter.eventually_ge_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
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 : α
⊢ 0 < c

Tactic:
have h₁ := hc_mem.1
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
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
rw : C = c * C / c
⊢ C = c * (C / c)

Tactic:
rw [← mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
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 ≠ 0

Tactic:
positivity