feat(analysis/normed_space/spectrum): adds easy direction of Gelfand's formula for the spectral radius (#10847)

This adds the easy direction (i.e., an inequality) of Gelfand's formula for the spectral radius. Namely, we prove that `spectral_radius 𝕜 a ≤ ∥a ^ (n + 1)∥₊ ^ (1 / (n + 1) : ℝ)` for all `n : ℕ` using the spectral mapping theorem for polynomials.

- [x] depends on: #10783

Author: j-loreaux

src/analysis/normed/group/basic.lean

@@ -543,6 +543,9 @@ instance semi_normed_group.to_has_nnnorm : has_nnnorm E := ⟨λ a, ⟨norm a, n
 
 @[simp, norm_cast] lemma coe_nnnorm (a : E) : (∥a∥₊ : ℝ) = norm a := rfl
 
+lemma norm_to_nnreal {a : E} : ∥a∥.to_nnreal = ∥a∥₊ :=
+@real.to_nnreal_coe ∥a∥₊
+
 lemma nndist_eq_nnnorm (a b : E) : nndist a b = ∥a - b∥₊ := nnreal.eq $ dist_eq_norm _ _
 
 @[simp] lemma nnnorm_zero : ∥(0 : E)∥₊ = 0 :=

src/analysis/normed_space/spectrum.lean

@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 import algebra.algebra.spectrum
 import analysis.calculus.deriv
+import analysis.special_functions.pow
 /-!
 # The spectrum of elements in a complete normed algebra
 
@@ -87,11 +88,26 @@ metric.is_compact_of_is_closed_bounded (is_closed a) (is_bounded a)
 
 theorem spectral_radius_le_nnnorm (a : A) :
   spectral_radius 𝕜 a ≤ ∥a∥₊ :=
+by { refine bsupr_le (λ k hk, _), exact_mod_cast norm_le_norm_of_mem hk }
+
+open ennreal polynomial
+
+theorem spectral_radius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) :
+  spectral_radius 𝕜 a ≤ ∥a ^ (n + 1)∥₊ ^ (1 / (n + 1) : ℝ) :=
 begin
-  suffices h : ∀ k ∈ σ a, (∥k∥₊ : ℝ≥0∞) ≤ ∥a∥₊,
-  { exact bsupr_le h, },
-  { intros _ hk,
-    exact_mod_cast norm_le_norm_of_mem hk },
+  refine bsupr_le (λ k hk, _),
+  /- apply easy direction of the spectral mapping theorem for polynomials -/
+  have pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1)),
+    by simpa only [one_mul, algebra.algebra_map_eq_smul_one, one_smul, aeval_monomial, one_mul,
+      eval_monomial] using subset_polynomial_aeval a (monomial (n + 1) (1 : 𝕜)) ⟨k, hk, rfl⟩,
+  /- power of the norm is bounded by norm of the power -/
+  have nnnorm_pow_le : (↑(∥k∥₊ ^ (n + 1)) : ℝ≥0∞) ≤ ↑∥a ^ (n + 1)∥₊,
+    by simpa only [norm_to_nnreal, normed_field.nnnorm_pow k (n+1)]
+      using coe_mono (real.to_nnreal_mono (norm_le_norm_of_mem pow_mem)),
+  /- take (n + 1)ᵗʰ roots and clean up the left-hand side -/
+  have hn : 0 < ((n + 1) : ℝ), by exact_mod_cast nat.succ_pos',
+  convert monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le,
+  erw [coe_pow, ←rpow_nat_cast, ←rpow_mul, mul_one_div_cancel hn.ne', rpow_one],
 end
 
 end spectrum_compact