awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
h : (↑‖k‖₊ : ℝ≥0∞) = (fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞)
h₁ :
  (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    (fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
      ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞))
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
convert! monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le using 1

Premises used: Iff.mpr, ENNReal.monotone_rpow_of_nonneg, LT.lt.le, one_div_pos
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
h : n + 1 ≠ 0
⊢ (↑‖k‖₊ : ℝ≥0∞) = ((↑‖k‖₊ : ℝ≥0∞) ^ (n + 1)) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
rw [one_div, pow_rpow_inv_natCast]

Premises used: ENNReal.pow_rpow_inv_natCast, one_div
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
⊢ n + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
h :
  (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h₁ h₂ :
  (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
rw [Nat.cast_succ, ENNReal.coe_mul_rpow]

Premises used: Nat.cast_succ, ENNReal.coe_mul_rpow
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop

Tactic:
ENNReal.le_of_forall_lt_one_mul_le fun ε hε => ?_

Premises used: ENNReal.le_of_forall_lt_one_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
refine :
  ∀ (ε : ℝ≥0∞) (hε : ε < 1),
    ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
⊢ spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop

Tactic:
refine ENNReal.le_of_forall_lt_one_mul_le fun ε hε => ?_

Premises used: ENNReal.le_of_forall_lt_one_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
pos :
  ∀ (h : ε = 0),
    ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
neg :
  ∀ (h : ¬ε = 0),
    ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop

Tactic:
by_cases h : ε = 0
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ε = 0
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
neg :
  spectralRadius 𝕜 a ≤
    ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop

Tactic:
simp only [ENNReal.mul_le_iff_le_inv h (hε.trans_le le_top).ne, mul_comm ε⁻¹,
    liminf_eq_iSup_iInf_of_nat', ENNReal.iSup_mul]

Premises used: Filter.liminf_eq_iSup_iInf_of_nat', ENNReal.mul_le_iff_le_inv, Inv.inv, LT.lt.trans_le, le_top, mul_comm, ENNReal.iSup_mul, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
arg : fun (i : ℕ) ↦ (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
| ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹

Tactic:
arg 1
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
i : ℕ
⊢ ε⁻¹ = ∞ →
    Eq (α := ℝ≥0∞) (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) 0 →
      ∃ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) = 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
i : ℕ
h₁ : ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
| (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹

Tactic:
rw [ENNReal.iInf_mul (by simp [h])]

Premises used: ENNReal.iInf_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
h₁ : ∀ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
| ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹

Tactic:
arg 1; intro i; rw [ENNReal.iInf_mul (by simp [h])]

Premises used: ENNReal.iInf_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
neg :
  spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
⊢ spectralRadius 𝕜 a ≤
    ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹

Tactic:
conv_rhs => arg 1; intro i; rw [ENNReal.iInf_mul (by simp [h])]

Premises used: ENNReal.iInf_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ 1 < ε⁻¹

Tactic:
rw [← ENNReal.inv_lt_inv, inv_one] at hε

Premises used: inv_one, ENNReal.inv_lt_inv
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
hε₁ : 1 < ε⁻¹
⊢ ¬ε = 0

Tactic:
rw [← ENNReal.inv_lt_inv, inv_one] at hε

Premises used: inv_one, ENNReal.inv_lt_inv
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
neg :
  ∀ (N : ℕ) (hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹),
    spectralRadius 𝕜 a ≤
      ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹

Tactic:
obtain ⟨N, hN⟩ := eventually_atTop.mp
    (ENNReal.eventually_pow_one_div_le (ENNReal.coe_ne_top : ↑‖(1 : A)‖₊ ≠ ∞) hε)

Premises used: ENNReal.eventually_pow_one_div_le, Iff.mp, Filter.eventually_atTop, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹

Tactic:
le_trans ?_ (le_iSup _ (N + 1))

Premises used: le_iSup, HAdd.hAdd, OfNat.ofNat, le_trans
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
neg : spectralRadius 𝕜 a ≤ ⨅ (i : ℕ), (↑‖a ^ (i + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i + (N + 1)) : ℝ) * ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹

Tactic:
refine le_trans ?_ (le_iSup _ (N + 1))

Premises used: le_iSup, HAdd.hAdd, OfNat.ofNat, le_trans
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨅ (i : ℕ), (↑‖a ^ (i + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i + (N + 1)) : ℝ) * ε⁻¹

Tactic:
le_iInf fun n => ?_

Premises used: le_iInf
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
neg : ∀ (n : ℕ), spectralRadius 𝕜 a ≤ (↑‖a ^ (n + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + (N + 1)) : ℝ) * ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨅ (i : ℕ), (↑‖a ^ (i + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i + (N + 1)) : ℝ) * ε⁻¹

Tactic:
refine le_iInf fun n => ?_

Premises used: le_iInf
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
neg : spectralRadius 𝕜 a ≤ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
⊢ spectralRadius 𝕜 a ≤ (↑‖a ^ (n + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + (N + 1)) : ℝ) * ε⁻¹

Tactic:
simp only [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
⊢ spectralRadius 𝕜 a ≤ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹

Tactic:
(spectralRadius_le_pow_nnnorm_pow_one_div 𝕜 a (n + N)).trans ?_

Premises used: HAdd.hAdd, LE.le.trans, spectrum.spectralRadius_le_pow_nnnorm_pow_one_div
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
neg :
  (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
⊢ spectralRadius 𝕜 a ≤ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹

Tactic:
refine (spectralRadius_le_pow_nnnorm_pow_one_div 𝕜 a (n + N)).trans ?_

Premises used: HAdd.hAdd, LE.le.trans, spectrum.spectralRadius_le_pow_nnnorm_pow_one_div
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
neg :
  (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
⊢ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
⊢ n + N + 1 ≥ N

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
neg neg₁ :
  (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹ ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
⊢ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹

Tactic:
grw [hN (n + N + 1) (by lia)]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
rw : ∃ (i : ℝ), True ∧ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Set.Ioi i) x → IsUnit (resolvent a x)
⊢ ∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)

Tactic:
rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]

Premises used: Filter.atTop_basis_Ioi, Filter.HasBasis.cobounded_of_norm, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ ∃ (i : ℝ), True ∧ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Set.Ioi i) x → IsUnit (resolvent a x)

Tactic:
⟨‖a‖ * ‖(1 : A)‖, trivial, fun _ ↦ isUnit_resolvent.mp ∘ mem_resolventSet_of_norm_lt_mul⟩

Premises used: Norm.norm, trivial, HMul.hMul, Function.comp, And.intro, Exists.intro, Iff.mp, OfNat.ofNat, spectrum.isUnit_resolvent, spectrum.mem_resolventSet_of_norm_lt_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ ∃ (i : ℝ), True ∧ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Set.Ioi i) x → IsUnit (resolvent a x)

Tactic:
exact ⟨‖a‖ * ‖(1 : A)‖, trivial, fun _ ↦ isUnit_resolvent.mp ∘ mem_resolventSet_of_norm_lt_mul⟩
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ Tendsto.{u_1, u_2} (β := A) (fun (x : 𝕜) ↦ x⁻¹ • a) (cobounded 𝕜) (𝓝 0)

Tactic:
simpa using (tendsto_inv₀_cobounded (α := 𝕜)).smul_const a

Premises used: Filter.tendsto_inv₀_cobounded, Filter.Tendsto.smul_const
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1

Tactic:
simpa [Function.comp_def, resolvent] using
      (NormedRing.inverse_one_sub_norm (R := A)).comp_tendsto
        (by simpa using (tendsto_inv₀_cobounded (α := 𝕜)).smul_const a)

Premises used: NormedRing.inverse_one_sub_norm, Function.comp_def, resolvent, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
h₁ :
  ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {0}ᶜ z), resolvent a z = z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1
⊢ resolvent a =ᶠ[cobounded 𝕜] fun (z : 𝕜) ↦ z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1

Tactic:
filter_upwards [isBounded_singleton (x := 0)] with z hz

Premises used: Bornology.isBounded_singleton
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {0}ᶜ z
⊢ IsUnit z

Tactic:
Ne.isUnit hz

Premises used: Ne.isUnit
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {0}ᶜ z
h₁ :
  ∀ (z : 𝕜ˣ) (hz : Membership.mem (γ := Set 𝕜) {0}ᶜ (↑z : 𝕜)),
    resolvent a (↑z : 𝕜) = (↑z : 𝕜)⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) ((↑z : 𝕜)⁻¹ • a) 1
⊢ resolvent a z = z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1

Tactic:
lift z to 𝕜ˣ using Ne.isUnit hz

Premises used: Ne.isUnit
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
z : 𝕜ˣ
hz : Membership.mem (γ := Set 𝕜) {0}ᶜ (↑z : 𝕜)
⊢ resolvent a (↑z : 𝕜) = (↑z : 𝕜)⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) ((↑z : 𝕜)⁻¹ • a) 1

Tactic:
simpa [Units.smul_def] using congr(z⁻¹ • $(units_smul_resolvent_self (r := z) (a := a)))

Premises used: spectrum.units_smul_resolvent_self, Units.smul_def
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
h :
  IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ 1
⊢ IsBigO.{u_1, u_2, 0} (E := A) (F := ℝ) (cobounded 𝕜) (fun (z : 𝕜) ↦ z⁻¹ • resolvent.{u_1, u_2} (R := 𝕜) (z⁻¹ • a) 1)
    fun (x : 𝕜) ↦ ‖x⁻¹‖

Tactic:
simpa using (isBigO_refl (· ⁻¹) (cobounded 𝕜)).norm_right.smul h

Premises used: Asymptotics.IsBigO.smul, Inv.inv, Bornology.cobounded, Asymptotics.IsBigO.norm_right, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ Tendsto (resolvent a) (cobounded 𝕜) (𝓝 0)

Tactic:
resolvent_isBigO_inv a |>.trans_tendsto tendsto_inv₀_cobounded

Premises used: Filter.tendsto_inv₀_cobounded, Asymptotics.IsBigO.trans_tendsto
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
⊢ (↑‖a‖₊ : ℝ≥0∞)⁻¹ ≤
    radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := A) fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)

Tactic:
le_of_forall_nnreal_lt fun r hr =>
        le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => ?_

Premises used: NNNorm.nnnorm, HPow.hPow, Max.max, ContinuousMultilinearMap.mkPiRing, ENNReal.le_of_forall_nnreal_lt, OfNat.ofNat, Fin, FormalMultilinearSeries.le_radius_of_bound_nnreal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
refine :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹) (n : ℕ),
    nnnorm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) A)
          (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) *
        r ^ n ≤
      max 1 (nnnorm.{u_2} (E := A) 1)
⊢ (↑‖a‖₊ : ℝ≥0∞)⁻¹ ≤
    radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := A) fun (n : ℕ) ↦ ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)

Tactic:
refine le_of_forall_nnreal_lt fun r hr =>
        le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => ?_

Premises used: NNNorm.nnnorm, Max.max, ENNReal.le_of_forall_nnreal_lt, OfNat.ofNat, FormalMultilinearSeries.le_radius_of_bound_nnreal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < (↑‖a‖₊ : ℝ≥0∞)⁻¹
n : ℕ
rw : ‖a ^ n‖₊ * r ^ n ≤ max 1 (nnnorm.{u_2} (E := A) 1)
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) A)
        (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) *
      r ^ n ≤
    max 1 (nnnorm.{u_2} (E := A) 1)

Tactic:
rw [← norm_toNNReal, norm_mkPiRing, norm_toNNReal]

Premises used: ContinuousMultilinearMap.norm_mkPiRing, norm_toNNReal