-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem limsup_pow_nnnorm_pow_one_div_le_spectralRadius (a : A) :
    limsup (fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) atTop ≤ spectralRadius ℂ a

Proof state:
case h.e'_4
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ liminf (fun i => 1 / ↑‖a ^ i‖.toNNReal ^ (1 / ↑i)) atTop = liminf (fun n => 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))) atTop

Tactic:
congr

Result:
case h.e'_4.e_u
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ (fun i => 1 / ↑‖a ^ i‖.toNNReal ^ (1 / ↑i)) = fun n => 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop

Tactic:
let p : FormalMultilinearSeries ℂ ℂ A := fun n =>
  ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)

Result:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ ↑r ≤ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop

Proof state:
case h.e'_4
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop = p.radius

Tactic:
simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]

Result:
case h.e'_4
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ liminf (fun i => 1 / ↑‖a ^ i‖.toNNReal ^ (1 / ↑i)) atTop = liminf (fun n => 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))) atTop

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ ↑r ≤ p.radius

Tactic:
have H₁ := (differentiableOn_inverse_one_sub_smul r_lt).hasFPowerSeriesOnBall r_pos

Result:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
H₁ :
  HasFPowerSeriesOnBall (fun z => Ring.inverse (1 - z • a)) (cauchyPowerSeries (fun z => Ring.inverse (1 - z • a)) 0 ↑r)
    0 ↑r
⊢ ↑r ≤ p.radius

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ ↑r ≤ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop

Tactic:
suffices h : (r : ℝ≥0∞) ≤ p.radius by
  convert h
  simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]
  congr
  ext n
  rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]
  exact fun ha => (lt_self_iff_false _).mp
    (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))

Result:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
⊢ ↑r ≤ p.radius

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
H₁ :
  HasFPowerSeriesOnBall (fun z => Ring.inverse (1 - z • a)) (cauchyPowerSeries (fun z => Ring.inverse (1 - z • a)) 0 ↑r)
    0 ↑r
⊢ ↑r ≤ p.radius

Tactic:
exact ((hasFPowerSeriesOnBall_inverse_one_sub_smul ℂ a).exchange_radius H₁).r_le

Result:
no goals

Proof state:
case h.e'_4.e_u.h
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ 1 / ↑‖a ^ n‖.toNNReal ^ (1 / ↑n) = 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))

Tactic:
rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]

Result:
case h.e'_4.e_u.h.hnc
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ ¬(‖a ^ n‖₊ = 0 ∧ 1 / ↑n < 0)

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ (limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop)⁻¹

Tactic:
simp_rw [inv_limsup, ← one_div]

Result:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
⊢ ↑r ≤ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ ↑r ≤ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop

Tactic:
convert h

Result:
case h.e'_4
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ liminf (fun i => 1 / ↑‖a ^ i‖₊ ^ (1 / ↑i)) atTop = p.radius

Proof state:
case h.e'_4.e_u
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
⊢ (fun i => 1 / ↑‖a ^ i‖.toNNReal ^ (1 / ↑i)) = fun n => 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))

Tactic:
ext n

Result:
case h.e'_4.e_u.h
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ 1 / ↑‖a ^ n‖.toNNReal ^ (1 / ↑n) = 1 / ↑(‖a ^ n‖.toNNReal ^ (1 / ↑n))

Proof state:
case h.e'_4.e_u.h.hnc
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ ¬(‖a ^ n‖₊ = 0 ∧ 1 / ↑n < 0)

Tactic:
exact fun ha => (lt_self_iff_false _).mp
  (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))

Result:
no goals