awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
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)⁻¹
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)⁻¹

Tactic:
simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]

Premises used: neg_div, mul_inv, div_eq_mul_inv, neg_inv, neg_mul
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (x : ℝ) ↦ (x * 1)⁻¹

Tactic:
IsLittleO.inv_rev ?_ ?_

Premises used: Asymptotics.IsLittleO.inv_rev
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
refine_1 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x * 1) fun (x : ℝ) ↦ -x * HPow.hPow (β := ℕ) (log x) 2
refine_2 : ∀ᶠ (x : ℝ) in atTop, x * 1 = 0 → -x * HPow.hPow (β := ℕ) (log x) 2 = 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ (-x * HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (x : ℝ) ↦ (x * 1)⁻¹

Tactic:
refine IsLittleO.inv_rev ?_ ?_

Premises used: Asymptotics.IsLittleO.inv_rev
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
rw : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x) fun (x : ℝ) ↦ x
⊢ IsBigO (E := ℝ) atTop (fun (x : ℝ) ↦ x) Neg.neg

Tactic:
rw [isBigO_neg_right]

Premises used: Asymptotics.isBigO_neg_right
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x) fun (x : ℝ) ↦ x

Tactic:
aesop (add safe isBigO_refl)

Premises used: Asymptotics.isBigO_refl
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
refine_1 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x * 1) fun (x : ℝ) ↦ -x * HPow.hPow (β := ℕ) (log x) 2

Tactic:
refine IsBigO.mul_isLittleO
          (by rw [isBigO_neg_right]; aesop (add safe isBigO_refl)) ?_

Premises used: Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
refine_1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖HPow.hPow (β := ℕ) (log x) 2‖) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2

Tactic:
rw [isLittleO_one_left_iff]

Premises used: Asymptotics.isLittleO_one_left_iff
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Ne (α := ℕ) 2 0

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖HPow.hPow (β := ℕ) (log x) 2‖) atTop atTop

Tactic:
exact Tendsto.comp tendsto_norm_atTop_atTop
          <| Tendsto.comp (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

Premises used: tendsto_norm_atTop_atTop, Real.tendsto_log_atTop, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : x * 1 = 0
⊢ x = 0

Tactic:
rw [mul_one] at hx

Premises used: mul_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : x = 0
⊢ -x * HPow.hPow (β := ℕ) (log x) 2 = 0

Tactic:
simp [hx]
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop, x * 1 = 0 → -x * HPow.hPow (β := ℕ) (log x) 2 = 0

Tactic:
exact Filter.Eventually.of_forall (fun x hx => by rw [mul_one] at hx; simp [hx])

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ (x * 1)⁻¹) fun (x : ℝ) ↦ x⁻¹

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 - ε x) x = (-deriv ε) x
⊢ (deriv fun (x : ℝ) ↦ 1 - ε x) =ᶠ[atTop] -deriv ε

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = (-deriv ε) x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
h₂ : DifferentiableAt ℝ ε x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = (-deriv ε) x

Tactic:
rw [deriv_fun_sub]

Premises used: deriv_fun_sub
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = (-deriv ε) x

Tactic:
aesop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x

Tactic:
aesop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε x

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

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

Tactic:
simp [deriv_smoothingFn, neg_div]

Premises used: neg_div, AkraBazziRecurrence.deriv_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
⊢ (deriv fun (x : ℝ) ↦ 1 + ε x) =ᶠ[atTop] deriv ε

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x + deriv ε x = deriv ε x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
h₂ : DifferentiableAt ℝ ε x
⊢ deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x

Tactic:
rw [deriv_fun_add]

Premises used: deriv_fun_add
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ 1) x + deriv ε x = deriv ε x

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

Tactic:
simp [deriv_smoothingFn]

Premises used: AkraBazziRecurrence.deriv_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 - ε x) x = -deriv ε x
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (x : ℝ) ↦ 1 - ε x) fun (z : ℝ) ↦ -deriv ε z

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
h : deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = -deriv ε x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1) x
h₂ : DifferentiableAt ℝ ε x
⊢ deriv (fun (x : ℝ) ↦ 1 - ε x) x = -deriv ε x

Tactic:
rw [deriv_fun_sub]

Premises used: deriv_fun_sub
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ 1) x - deriv ε x = -deriv ε x

Tactic:
aesop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
rw : IsLittleO (F := ℝ) atTop (deriv ε) fun (x : ℝ) ↦ x⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -deriv ε z) fun (x : ℝ) ↦ x⁻¹

Tactic:
rw [isLittleO_neg_left]

Premises used: Asymptotics.isLittleO_neg_left
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsLittleO (F := ℝ) atTop (deriv ε) fun (x : ℝ) ↦ x⁻¹

Tactic:
isLittleO_deriv_smoothingFn

Premises used: AkraBazziRecurrence.isLittleO_deriv_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsLittleO (F := ℝ) atTop (deriv ε) fun (x : ℝ) ↦ x⁻¹

Tactic:
exact isLittleO_deriv_smoothingFn

Premises used: AkraBazziRecurrence.isLittleO_deriv_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h : ∀ (x : ℝ) (hx : 1 < x), deriv (fun (x : ℝ) ↦ 1 + ε x) x = deriv ε x
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (x : ℝ) ↦ 1 + ε x) fun (z : ℝ) ↦ deriv ε z

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ IsLittleO (F := ℝ) atTop ε fun (x : ℝ) ↦ 1

Tactic:
have h₁ := isLittleO_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : IsLittleO (F := ℝ) atTop ε fun (x : ℝ) ↦ 1
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1

Tactic:
rw [isLittleO_iff] at h₁

Premises used: Asymptotics.isLittleO_iff
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε (↑n : ℝ)

Tactic:
Eventually.natCast_atTop (p := fun n => 0 < 1 + ε n) ?_

Premises used: Filter.Eventually.natCast_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
refine : ∀ᶠ (x : ℝ) in atTop, (fun (n : ℝ) ↦ 0 < 1 + ε n) x
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε (↑n : ℝ)

Tactic:
refine Eventually.natCast_atTop (p := fun n => 0 < 1 + ε n) ?_

Premises used: Filter.Eventually.natCast_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
x : ℝ
h : ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1 → 1 < x → 0 < 1 + ε x
⊢ ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1 → 1 < x → 0 < 1 + ε x

Tactic:
_
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
h : ∀ (x : ℝ), ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1 → ∀ (hx' : 1 < x), 0 < 1 + ε x
⊢ ∀ᶠ (x : ℝ) in atTop, (fun (n : ℝ) ↦ 0 < 1 + ε n) x

Tactic:
filter_upwards [h₁ (by simp : (0 : ℝ) < 1 / 2), eventually_gt_atTop 1] with x _ hx'

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
x : ℝ
h : ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1
hx' : 1 < x
⊢ 0 < log x

Tactic:
have : 0 < log x := Real.log_pos hx'
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * Norm.norm (E := ℝ) 1
x : ℝ
h : ‖ε x‖ ≤ 1 / 2 * Norm.norm (E := ℝ) 1
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + 1 / log x

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

Tactic:
rw [Filter.eventually_all]

Premises used: Filter.eventually_all
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 + ε (↑(r i x) : ℝ)

Tactic:
fun i => (R.tendsto_atTop_r i).eventually (f := r i) eventually_one_add_smoothingFn_pos

Premises used: AkraBazziRecurrence.tendsto_atTop_r, Filter.Tendsto.eventually, AkraBazziRecurrence.eventually_one_add_smoothingFn_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
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 + ε (↑(r i x) : ℝ)

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually (f := r i) eventually_one_add_smoothingFn_pos

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

Tactic:
filter_upwards [eventually_one_add_smoothingFn_pos] with n hn

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

Tactic:
le_of_lt hn

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

Tactic:
exact le_of_lt hn

Premises used: le_of_lt
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
simp_rw : StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (Set.Ioi 1)
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ 1 / log x) (Set.Ioi 1)

Tactic:
simp_rw [one_div]

Premises used: one_div
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (Set.Ioi 1)

Tactic:
StrictAntiOn.comp_strictMonoOn inv_strictAntiOn ?log fun _ hx => log_pos hx

Premises used: inv_strictAntiOn, StrictAntiOn.comp_strictMonoOn, Real.log_pos
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
log : StrictMonoOn Real.log (Set.Ioi 1)
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ (Real.log x)⁻¹) (Set.Ioi 1)

Tactic:
refine StrictAntiOn.comp_strictMonoOn inv_strictAntiOn ?log fun _ hx => log_pos hx
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ StrictMonoOn log (Set.Ioi 1)

Tactic:
StrictMonoOn.mono strictMonoOn_log (fun x hx => ?_)

Premises used: StrictMonoOn.mono, Real.strictMonoOn_log
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
log : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioi 1) x), Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ StrictMonoOn Real.log (Set.Ioi 1)

Tactic:
refine StrictMonoOn.mono strictMonoOn_log (fun x hx => ?_)

Premises used: StrictMonoOn.mono, Real.strictMonoOn_log
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x

Tactic:
Set.Ioi_subset_Ioi zero_le_one hx

Premises used: zero_le_one, Set.Ioi_subset_Ioi
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x

Tactic:
exact Set.Ioi_subset_Ioi zero_le_one hx

Premises used: zero_le_one, Set.Ioi_subset_Ioi
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ 1 + -ε x) (Set.Ioi 1)

Tactic:
StrictMonoOn.const_add (StrictAntiOn.neg <| strictAntiOn_smoothingFn) 1

Premises used: StrictAntiOn.neg, OfNat.ofNat, StrictMonoOn.const_add, AkraBazziRecurrence.strictAntiOn_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ 1 + -ε x) (Set.Ioi 1)

Tactic:
exact StrictMonoOn.const_add (StrictAntiOn.neg <| strictAntiOn_smoothingFn) 1

Premises used: StrictAntiOn.neg, OfNat.ofNat, StrictMonoOn.const_add, AkraBazziRecurrence.strictAntiOn_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ 1 + ε x) (Set.Ioi 1)

Tactic:
StrictAntiOn.const_add strictAntiOn_smoothingFn 1

Premises used: StrictAntiOn.const_add, OfNat.ofNat, AkraBazziRecurrence.strictAntiOn_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
h :
  ∀ (n : ℕ) (hn : 1 < n) (hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))),
    1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ) =
      (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
⊢ EventuallyEq (β := ℝ) atTop (fun (n : ℕ) ↦ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ)) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))

Tactic:
filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'

Premises used: AkraBazziRecurrence.eventually_log_b_mul_pos, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)

Tactic:
simp_all
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
⊢ 0 < log (↑n : ℝ)

Tactic:
have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
h :
  (log (b i * (↑n : ℝ)))⁻¹ - (log (↑n : ℝ))⁻¹ =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
⊢ 1 / log (b i * (↑n : ℝ)) - 1 / log (↑n : ℝ) =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))

Tactic:
simp only [one_div]

Premises used: one_div
-- 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 : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
⊢ 0 < log (b i * (↑n : ℝ))

Tactic:
have := 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
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
this : 0 < log (b i * (↑n : ℝ))
⊢ log (b i * (↑n : ℝ)) ≠ 0

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
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
⊢ log (↑n : ℝ) ≠ 0

Tactic:
aesop
-- 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 : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * (↑n : ℝ))
h_log_pos : 0 < log (↑n : ℝ)
h h₁ :
  (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))
⊢ (log (b i * (↑n : ℝ)))⁻¹ - (log (↑n : ℝ))⁻¹ =
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))

Tactic:
rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]

Premises used: inv_sub_inv
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
h :
  ∀ (n : ℕ) (hn : n ≠ 0),
    (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
      (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Premises used: Filter.eventually_ne_atTop, 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
i : α
n : ℕ
hn : n ≠ 0
⊢ 0 < b i

Tactic:
have : 0 < b i := R.b_pos 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 : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ b i ≠ 0

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
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
simp_all
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
this : 0 < b i
h :
  (log (↑n : ℝ) - (log (b i) + log (↑n : ℝ))) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
h₁ h₂ :
  (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))
⊢ (log (↑n : ℝ) - log (b i * (↑n : ℝ))) / (log (b i * (↑n : ℝ)) * log (↑n : ℝ)) =
    (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))

Tactic:
rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]

Premises used: sub_add_eq_sub_sub, Real.log_mul
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
h :
  ∀ (x : ℕ),
    (log (↑x : ℝ) - log (b i) - log (↑x : ℝ)) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ)) =
      -log (b i) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ))
⊢ Eq (α := (n : ℕ) → ℝ)
    (fun (n : ℕ) ↦ (log (↑n : ℝ) - log (b i) - log (↑n : ℝ)) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ)))
    fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))

Tactic:
ext
-- 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 : ℕ
h : log (↑x : ℝ) - log (b i) - log (↑x : ℝ) = -log (b i)
⊢ (log (↑x : ℝ) - log (b i) - log (↑x : ℝ)) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ)) =
    -log (b i) / ((log (b i) + log (↑x : ℝ)) * log (↑x : ℝ))

Tactic:
congr
-- 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 : ℕ
⊢ log (↑x : ℝ) - log (b i) - log (↑x : ℝ) = -log (b i)

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
i : α
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))

Tactic:
IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)

Premises used: Asymptotics.IsEquivalent.mul, Asymptotics.IsEquivalent.div, Asymptotics.IsEquivalent.refl
-- 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 : α
refine : IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ log (b i) + log (↑n : ℝ)) fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ -log (b i) / ((log (b i) + log (↑n : ℝ)) * log (↑n : ℝ))) fun (n : ℕ) ↦
    -log (b i) / (log (↑n : ℝ) * log (↑n : ℝ))

Tactic:
refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)

Premises used: Asymptotics.IsEquivalent.mul, Asymptotics.IsEquivalent.div