refactor(analysis/normed_space/spectrum): remove norm_one_class hyp…

…otheses (#16891)

When this file and its main results were created, mathlib had a different definition of `normed_algebra` which automatically entailed `norm_one_class`. When `normed_algebra` was refactored, this hypothesis was added everywhere it was needed, including this file. However, most of the main results here are independent of that assumption, but the proof requires slightly more work. 

Here, we do that work so that we can remove these hypotheses here and a few places downstream. For a few results, we provide both the `norm_one_class` version, and the version without it for convenience (especially because any nontrivial cstar_ring automatically satisfies `norm_one_class`).

src/analysis/normed_space/algebra.lean

@@ -33,25 +33,21 @@ namespace weak_dual
 namespace character_space
 
 variables [nontrivially_normed_field 𝕜] [normed_ring A]
-  [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A]
+  [normed_algebra 𝕜 A] [complete_space A]
 
-lemma norm_one (φ : character_space 𝕜 A) : ∥to_normed_dual (φ : weak_dual 𝕜 A)∥ = 1 :=
-begin
-  refine continuous_linear_map.op_norm_eq_of_bounds zero_le_one (λ a, _) (λ x hx h, _),
-  { rw [one_mul],
-    exact spectrum.norm_le_norm_of_mem (apply_mem_spectrum φ a) },
-  { have : ∥φ 1∥ ≤ x * ∥(1 : A)∥ := h 1,
-    simpa only [norm_one, mul_one, map_one] using this },
-end
+lemma norm_le_norm_one (φ : character_space 𝕜 A) :
+  ∥to_normed_dual (φ : weak_dual 𝕜 A)∥ ≤ ∥(1 : A)∥ :=
+continuous_linear_map.op_norm_le_bound _ (norm_nonneg (1 : A)) $
+  λ a, mul_comm (∥a∥) (∥(1 : A)∥) ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ a)
 
 instance [proper_space 𝕜] : compact_space (character_space 𝕜 A) :=
 begin
   rw [←is_compact_iff_compact_space],
-  have h : character_space 𝕜 A ⊆ to_normed_dual ⁻¹' metric.closed_ball 0 1,
+  have h : character_space 𝕜 A ⊆ to_normed_dual ⁻¹' metric.closed_ball 0 (∥(1 : A)∥),
   { intros φ hφ,
     rw [set.mem_preimage, mem_closed_ball_zero_iff],
-    exact (le_of_eq $ norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _), },
-  exact compact_of_is_closed_subset (is_compact_closed_ball 𝕜 0 1) character_space.is_closed h,
+    exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _), },
+  exact compact_of_is_closed_subset (is_compact_closed_ball 𝕜 0 _) character_space.is_closed h,
 end
 
 end character_space

src/analysis/normed_space/spectrum.lean

@@ -58,12 +58,21 @@ namespace spectrum
 
 section spectrum_compact
 
+open filter
+
 variables [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A]
 
 local notation `σ` := spectrum 𝕜
 local notation `ρ` := resolvent_set 𝕜
 local notation `↑ₐ` := algebra_map 𝕜 A
 
+@[simp] lemma spectral_radius.of_subsingleton [subsingleton A] (a : A) :
+  spectral_radius 𝕜 a = 0 :=
+by simp [spectral_radius]
+
+@[simp] lemma spectral_radius_zero : spectral_radius 𝕜 (0 : A) = 0 :=
+by { nontriviality A, simp [spectral_radius] }
+
 lemma mem_resolvent_set_of_spectral_radius_lt {a : A} {k : 𝕜} (h : spectral_radius 𝕜 a < ∥k∥₊) :
   k ∈ ρ a :=
 not_not.mp $ λ hn, h.not_le $ le_supr₂ k hn
@@ -73,32 +82,48 @@ variable [complete_space A]
 lemma is_open_resolvent_set (a : A) : is_open (ρ a) :=
 units.is_open.preimage ((continuous_algebra_map 𝕜 A).sub continuous_const)
 
-lemma is_closed (a : A) : is_closed (σ a) :=
+protected lemma is_closed (a : A) : is_closed (σ a) :=
 (is_open_resolvent_set a).is_closed_compl
 
-lemma mem_resolvent_of_norm_lt [norm_one_class A] {a : A} {k : 𝕜} (h : ∥a∥ < ∥k∥) :
+lemma mem_resolvent_set_of_norm_lt_mul {a : A} {k : 𝕜} (h : ∥a∥ * ∥(1 : A)∥ < ∥k∥) :
   k ∈ ρ a :=
 begin
   rw [resolvent_set, set.mem_set_of_eq, algebra.algebra_map_eq_smul_one],
-  have hk : k ≠ 0 := ne_zero_of_norm_ne_zero (by linarith [norm_nonneg a]),
+  nontriviality A,
+  have hk : k ≠ 0,
+    from ne_zero_of_norm_ne_zero ((mul_nonneg (norm_nonneg _) (norm_nonneg _)).trans_lt h).ne',
   let ku := units.map (↑ₐ).to_monoid_hom (units.mk0 k hk),
-  have hku : ∥-a∥ < ∥(↑ku⁻¹:A)∥⁻¹ := by simpa [ku, algebra_map_isometry] using h,
+  rw [←inv_inv (∥(1 : A)∥), mul_inv_lt_iff (inv_pos.2 $ norm_pos_iff.2 (one_ne_zero : (1 : A) ≠ 0))]
+    at h,
+  have hku : ∥-a∥ < ∥(↑ku⁻¹:A)∥⁻¹ := by simpa [ku, norm_algebra_map] using h,
   simpa [ku, sub_eq_add_neg, algebra.algebra_map_eq_smul_one] using (ku.add (-a) hku).is_unit,
 end
 
+lemma mem_resolvent_set_of_norm_lt [norm_one_class A] {a : A} {k : 𝕜} (h : ∥a∥ < ∥k∥) :
+  k ∈ ρ a :=
+mem_resolvent_set_of_norm_lt_mul (by rwa [norm_one, mul_one])
+
+lemma norm_le_norm_mul_of_mem {a : A} {k : 𝕜} (hk : k ∈ σ a) :
+  ∥k∥ ≤ ∥a∥ * ∥(1 : A)∥ :=
+le_of_not_lt $ mt mem_resolvent_set_of_norm_lt_mul hk
+
 lemma norm_le_norm_of_mem [norm_one_class A] {a : A} {k : 𝕜} (hk : k ∈ σ a) :
   ∥k∥ ≤ ∥a∥ :=
-le_of_not_lt $ mt mem_resolvent_of_norm_lt hk
+le_of_not_lt $ mt mem_resolvent_set_of_norm_lt hk
+
+lemma subset_closed_ball_norm_mul (a : A) :
+  σ a ⊆ metric.closed_ball (0 : 𝕜) (∥a∥ * ∥(1 : A)∥) :=
+λ k hk, by simp [norm_le_norm_mul_of_mem hk]
 
 lemma subset_closed_ball_norm [norm_one_class A] (a : A) :
   σ a ⊆ metric.closed_ball (0 : 𝕜) (∥a∥) :=
 λ k hk, by simp [norm_le_norm_of_mem hk]
 
-lemma is_bounded [norm_one_class A] (a : A) : metric.bounded (σ a) :=
-(metric.bounded_iff_subset_ball 0).mpr ⟨∥a∥, subset_closed_ball_norm a⟩
+lemma is_bounded (a : A) : metric.bounded (σ a) :=
+(metric.bounded_iff_subset_ball 0).mpr ⟨∥a∥ * ∥(1 : A)∥, subset_closed_ball_norm_mul a⟩
 
-theorem is_compact [norm_one_class A] [proper_space 𝕜] (a : A) : is_compact (σ a) :=
-metric.is_compact_of_is_closed_bounded (is_closed a) (is_bounded a)
+protected theorem is_compact [proper_space 𝕜] (a : A) : is_compact (σ a) :=
+metric.is_compact_of_is_closed_bounded (spectrum.is_closed a) (is_bounded a)
 
 theorem spectral_radius_le_nnnorm [norm_one_class A] (a : A) :
   spectral_radius 𝕜 a ≤ ∥a∥₊ :=
@@ -107,22 +132,44 @@ by { refine supr₂_le (λ k hk, _), exact_mod_cast norm_le_norm_of_mem hk }
 open ennreal polynomial
 
 variable (𝕜)
-theorem spectral_radius_le_pow_nnnorm_pow_one_div [norm_one_class A] (a : A) (n : ℕ) :
-  spectral_radius 𝕜 a ≤ ∥a ^ (n + 1)∥₊ ^ (1 / (n + 1) : ℝ) :=
+theorem spectral_radius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) :
+  spectral_radius 𝕜 a ≤ (∥a ^ (n + 1)∥₊) ^ (1 / (n + 1) : ℝ) * (∥(1 : A)∥₊) ^ (1 / (n + 1) : ℝ) :=
 begin
   refine supr₂_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, nnnorm_pow k (n+1)]
-      using coe_mono (real.to_nnreal_mono (norm_le_norm_of_mem pow_mem)),
+  have nnnorm_pow_le : (↑(∥k∥₊ ^ (n + 1)) : ℝ≥0∞) ≤ ∥a ^ (n + 1)∥₊ * ∥(1 : A)∥₊,
+    { simpa only [real.to_nnreal_mul (norm_nonneg _), norm_to_nnreal, nnnorm_pow k (n + 1),
+        ennreal.coe_mul] using coe_mono (real.to_nnreal_mono (norm_le_norm_mul_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], rw nat.cast_succ,
+  erw [coe_pow, ←rpow_nat_cast, ←rpow_mul, mul_one_div_cancel hn.ne', rpow_one],
+  rw [nat.cast_succ, ennreal.coe_mul_rpow],
+end
+
+theorem spectral_radius_le_liminf_pow_nnnorm_pow_one_div (a : A) :
+  spectral_radius 𝕜 a ≤ at_top.liminf (λ n : ℕ, (∥a ^ n∥₊ : ℝ≥0∞) ^ (1 / n : ℝ)) :=
+begin
+  refine ennreal.le_of_forall_lt_one_mul_le (λ ε hε, _),
+  by_cases ε = 0,
+  { simp only [h, zero_mul, zero_le'] },
+  have hε' : ε⁻¹ ≠ ∞,
+    from λ h', h (by simpa only [inv_inv, inv_top] using congr_arg (λ (x : ℝ≥0∞), x⁻¹) h'),
+  simp only [ennreal.mul_le_iff_le_inv h (hε.trans_le le_top).ne, mul_comm ε⁻¹,
+    liminf_eq_supr_infi_of_nat', ennreal.supr_mul, ennreal.infi_mul hε'],
+  rw [←ennreal.inv_lt_inv, inv_one] at hε,
+  obtain ⟨N, hN⟩ := eventually_at_top.mp
+    (ennreal.eventually_pow_one_div_le (ennreal.coe_ne_top : ↑∥(1 : A)∥₊ ≠ ∞) hε),
+  refine (le_trans _ (le_supr _ (N + 1))),
+  refine le_infi (λ n, _),
+  simp only [←add_assoc],
+  refine (spectral_radius_le_pow_nnnorm_pow_one_div 𝕜 a (n + N)).trans _,
+  norm_cast,
+  exact mul_le_mul_left' (hN (n + N + 1) (by linarith)) _,
 end
 
 end spectrum_compact
@@ -283,22 +330,16 @@ end
 
 /-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
 `spectral_radius` of `a` is the limit of the sequence `∥a ^ n∥₊ ^ (1 / n)` -/
-theorem pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius [norm_one_class A] (a : A) :
+theorem pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius (a : A) :
   tendsto (λ n : ℕ, ((∥a ^ n∥₊ ^ (1 / n : ℝ)) : ℝ≥0∞)) at_top (𝓝 (spectral_radius ℂ a)) :=
-begin
-  refine tendsto_of_le_liminf_of_limsup_le _ _ (by apply_auto_param) (by apply_auto_param),
-  { rw [←liminf_nat_add _ 1, liminf_eq_supr_infi_of_nat],
-    refine le_trans _ (le_supr _ 0),
-    simp only [nat.cast_succ],
-    exact le_infi₂ (λ i hi, spectral_radius_le_pow_nnnorm_pow_one_div ℂ a i) },
-  { exact limsup_pow_nnnorm_pow_one_div_le_spectral_radius a },
-end
+tendsto_of_le_liminf_of_limsup_le (spectral_radius_le_liminf_pow_nnnorm_pow_one_div ℂ a)
+  (limsup_pow_nnnorm_pow_one_div_le_spectral_radius a)
 
 /- This is the same as `pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius` but for `norm`
 instead of `nnnorm`. -/
 /-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
 `spectral_radius` of `a` is the limit of the sequence `∥a ^ n∥₊ ^ (1 / n)` -/
-theorem pow_norm_pow_one_div_tendsto_nhds_spectral_radius [norm_one_class A] (a : A) :
+theorem pow_norm_pow_one_div_tendsto_nhds_spectral_radius (a : A) :
   tendsto (λ n : ℕ,  ennreal.of_real (∥a ^ n∥ ^ (1 / n : ℝ))) at_top (𝓝 (spectral_radius ℂ a)) :=
 begin
   convert pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius a,
@@ -423,20 +464,19 @@ section normed_field
 variables [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
 local notation `↑ₐ` := algebra_map 𝕜 A
 
-
 /-- An algebra homomorphism into the base field, as a continuous linear map (since it is
 automatically bounded). -/
-instance [norm_one_class A] : continuous_linear_map_class (A →ₐ[𝕜] 𝕜) 𝕜 A 𝕜 :=
-{ map_continuous := λ φ, add_monoid_hom_class.continuous_of_bound φ 1 $
-    λ a, (one_mul ∥a∥).symm ▸ spectrum.norm_le_norm_of_mem (apply_mem_spectrum φ _),
+instance : continuous_linear_map_class (A →ₐ[𝕜] 𝕜) 𝕜 A 𝕜 :=
+{ map_continuous := λ φ, add_monoid_hom_class.continuous_of_bound φ ∥(1 : A)∥ $
+    λ a, (mul_comm ∥a∥ ∥(1 : A)∥) ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ _),
   .. alg_hom_class.linear_map_class }
 
 /-- An algebra homomorphism into the base field, as a continuous linear map (since it is
 automatically bounded). -/
-def to_continuous_linear_map [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
+def to_continuous_linear_map (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
 { cont := map_continuous φ, .. φ.to_linear_map }
 
-@[simp] lemma coe_to_continuous_linear_map [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) :
+@[simp] lemma coe_to_continuous_linear_map (φ : A →ₐ[𝕜] 𝕜) :
   ⇑φ.to_continuous_linear_map = φ := rfl
 
 end normed_field
@@ -459,7 +499,7 @@ namespace weak_dual
 
 namespace character_space
 
-variables [normed_field 𝕜] [normed_ring A] [complete_space A] [norm_one_class A]
+variables [nontrivially_normed_field 𝕜] [normed_ring A] [complete_space A]
 variables [normed_algebra 𝕜 A]
 
 /-- The equivalence between characters and algebra homomorphisms into the base field. -/

src/analysis/normed_space/star/gelfand_duality.lean

@@ -59,7 +59,7 @@ section complex_banach_algebra
 open ideal
 
 variables {A : Type*} [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A]
-  [norm_one_class A] (I : ideal A) [ideal.is_maximal I]
+  (I : ideal A) [ideal.is_maximal I]
 
 /-- Every maximal ideal in a commutative complex Banach algebra gives rise to a character on that
 algebra. In particular, the character, which may be identified as an algebra homomorphism due to
@@ -101,23 +101,20 @@ begin
   exact (continuous_map.spectrum_eq_range (gelfand_transform ℂ A a)).symm ▸ ⟨f, hf.symm⟩,
 end
 
-instance : nonempty (character_space ℂ A) :=
-begin
-  haveI := norm_one_class.nontrivial A,
-  exact ⟨classical.some $
-    weak_dual.character_space.exists_apply_eq_zero (zero_mem_nonunits.mpr zero_ne_one)⟩,
-end
+instance [nontrivial A] : nonempty (character_space ℂ A) :=
+⟨classical.some $ weak_dual.character_space.exists_apply_eq_zero $ zero_mem_nonunits.2 zero_ne_one⟩
 
 end complex_banach_algebra
 
 section complex_cstar_algebra
 
 variables (A : Type*) [normed_comm_ring A] [normed_algebra ℂ A] [complete_space A]
-variables [star_ring A] [cstar_ring A] [star_module ℂ A] [nontrivial A]
+variables [star_ring A] [cstar_ring A] [star_module ℂ A]
 
 /-- The Gelfand transform is an isometry when the algebra is a C⋆-algebra over `ℂ`. -/
 lemma gelfand_transform_isometry : isometry (gelfand_transform ℂ A) :=
 begin
+  nontriviality A,
   refine add_monoid_hom_class.isometry_of_norm (gelfand_transform ℂ A) (λ a, _),
   have gt_map_star : gelfand_transform ℂ A (star a) = star (gelfand_transform ℂ A a),
     from continuous_map.ext (λ φ, map_star φ a),

src/analysis/normed_space/star/spectrum.lean

@@ -25,11 +25,12 @@ section unitary_spectrum
 variables
 {𝕜 : Type*} [normed_field 𝕜]
 {E : Type*} [normed_ring E] [star_ring E] [cstar_ring E]
-[normed_algebra 𝕜 E] [complete_space E] [nontrivial E]
+[normed_algebra 𝕜 E] [complete_space E]
 
 lemma unitary.spectrum_subset_circle (u : unitary E) :
   spectrum 𝕜 (u : E) ⊆ metric.sphere 0 1 :=
 begin
+  nontriviality E,
   refine λ k hk, mem_sphere_zero_iff_norm.mpr (le_antisymm _ _),
   { simpa only [cstar_ring.norm_coe_unitary u] using norm_le_norm_of_mem hk },
   { rw ←unitary.coe_to_units_apply u at hk,
@@ -54,7 +55,7 @@ variables {A : Type*}
 
 local notation `↑ₐ` := algebra_map ℂ A
 
-lemma is_self_adjoint.spectral_radius_eq_nnnorm [norm_one_class A] {a : A}
+lemma is_self_adjoint.spectral_radius_eq_nnnorm {a : A}
   (ha : is_self_adjoint a) :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
@@ -68,7 +69,7 @@ begin
   simp,
 end
 
-lemma is_star_normal.spectral_radius_eq_nnnorm [norm_one_class A] (a : A) [is_star_normal a] :
+lemma is_star_normal.spectral_radius_eq_nnnorm (a : A) [is_star_normal a] :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
   refine (ennreal.pow_strict_mono two_ne_zero).injective _,
@@ -86,7 +87,7 @@ begin
 end
 
 /-- Any element of the spectrum of a selfadjoint is real. -/
-theorem is_self_adjoint.mem_spectrum_eq_re [star_module ℂ A] [nontrivial A] {a : A}
+theorem is_self_adjoint.mem_spectrum_eq_re [star_module ℂ A] {a : A}
   (ha : is_self_adjoint a) {z : ℂ} (hz : z ∈ spectrum ℂ a) : z = z.re :=
 begin
   let Iu := units.mk0 I I_ne_zero,
@@ -100,19 +101,19 @@ begin
 end
 
 /-- Any element of the spectrum of a selfadjoint is real. -/
-theorem self_adjoint.mem_spectrum_eq_re [star_module ℂ A] [nontrivial A]
+theorem self_adjoint.mem_spectrum_eq_re [star_module ℂ A]
   (a : self_adjoint A) {z : ℂ} (hz : z ∈ spectrum ℂ (a : A)) : z = z.re :=
 a.prop.mem_spectrum_eq_re hz
 
 /-- The spectrum of a selfadjoint is real -/
-theorem is_self_adjoint.coe_re_map_spectrum [star_module ℂ A] [nontrivial A] {a : A}
+theorem is_self_adjoint.coe_re_map_spectrum [star_module ℂ A] {a : A}
   (ha : is_self_adjoint a) : spectrum ℂ a = (coe ∘ re '' (spectrum ℂ a) : set ℂ) :=
 le_antisymm (λ z hz, ⟨z, hz, (ha.mem_spectrum_eq_re hz).symm⟩) (λ z, by
   { rintros ⟨z, hz, rfl⟩,
     simpa only [(ha.mem_spectrum_eq_re hz).symm, function.comp_app] using hz })
 
 /-- The spectrum of a selfadjoint is real -/
-theorem self_adjoint.coe_re_map_spectrum [star_module ℂ A] [nontrivial A] (a : self_adjoint A) :
+theorem self_adjoint.coe_re_map_spectrum [star_module ℂ A] (a : self_adjoint A) :
   spectrum ℂ (a : A) = (coe ∘ re '' (spectrum ℂ (a : A)) : set ℂ) :=
 a.property.coe_re_map_spectrum
 
@@ -121,10 +122,8 @@ end complex_scalars
 namespace star_alg_hom
 
 variables {F A B : Type*}
-[normed_ring A] [normed_algebra ℂ A] [norm_one_class A]
-[complete_space A] [star_ring A] [cstar_ring A]
-[normed_ring B] [normed_algebra ℂ B] [norm_one_class B]
-[complete_space B] [star_ring B] [cstar_ring B]
+[normed_ring A] [normed_algebra ℂ A] [complete_space A] [star_ring A] [cstar_ring A]
+[normed_ring B] [normed_algebra ℂ B] [complete_space B] [star_ring B] [cstar_ring B]
 [hF : star_alg_hom_class F ℂ A B] (φ : F)
 include hF
 
@@ -161,7 +160,7 @@ namespace weak_dual
 open continuous_map complex
 open_locale complex_star_module
 
-variables {F A : Type*} [normed_ring A] [normed_algebra ℂ A] [nontrivial A] [complete_space A]
+variables {F A : Type*} [normed_ring A] [normed_algebra ℂ A] [complete_space A]
   [star_ring A] [cstar_ring A] [star_module ℂ A] [hF : alg_hom_class F ℂ A ℂ]
 
 include hF

src/analysis/special_functions/pow.lean

@@ -1442,6 +1442,16 @@ begin
   rw [←nnreal.coe_rpow, real.to_nnreal_coe],
 end
 
+lemma eventually_pow_one_div_le (x : ℝ≥0) {y : ℝ≥0} (hy : 1 < y) :
+  ∀ᶠ (n : ℕ) in at_top, x ^ (1 / n : ℝ) ≤ y :=
+begin
+  obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy),
+  rw [tsub_add_cancel_of_le hy.le] at hm,
+  refine eventually_at_top.2 ⟨m + 1, λ n hn, _⟩,
+  simpa only [nnreal.rpow_one_div_le_iff (nat.cast_pos.2 $ m.succ_pos.trans_le hn),
+    nnreal.rpow_nat_cast] using hm.le.trans (pow_le_pow hy.le (m.le_succ.trans hn)),
+end
+
 end nnreal
 
 namespace real
@@ -2003,6 +2013,18 @@ begin
   exact_mod_cast hc a (by exact_mod_cast ha),
 end
 
+lemma eventually_pow_one_div_le {x : ℝ≥0∞} (hx : x ≠ ∞) {y : ℝ≥0∞} (hy : 1 < y) :
+  ∀ᶠ (n : ℕ) in at_top, x ^ (1 / n : ℝ) ≤ y :=
+begin
+  lift x to ℝ≥0 using hx,
+  by_cases y = ∞,
+  { exact eventually_of_forall (λ n, h.symm ▸ le_top) },
+  { lift y to ℝ≥0 using h,
+    have := nnreal.eventually_pow_one_div_le x (by exact_mod_cast hy : 1 < y),
+    refine this.congr (eventually_of_forall $ λ n, _),
+    rw [coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe] },
+end
+
 private lemma continuous_at_rpow_const_of_pos {x : ℝ≥0∞} {y : ℝ} (h : 0 < y) :
   continuous_at (λ a : ℝ≥0∞, a ^ y) x :=
 begin

src/topology/algebra/module/character_space.lean

@@ -87,6 +87,9 @@ def to_non_unital_alg_hom (φ : character_space 𝕜 A) : A →ₙₐ[𝕜] 𝕜
 @[simp]
 lemma coe_to_non_unital_alg_hom (φ : character_space 𝕜 A) : ⇑(to_non_unital_alg_hom φ) = φ := rfl
 
+instance [subsingleton A] : is_empty (character_space 𝕜 A) :=
+⟨λ φ, φ.prop.1 $ continuous_linear_map.ext (λ x, by simp only [subsingleton.elim x 0, map_zero])⟩
+
 variables (𝕜 A)
 
 lemma union_zero :