The spectrum of elements in a complete normed algebra

This file contains the basic theory for the resolvent and spectrum of a Banach algebra.

Main definitions

• spectralRadius : ℝ≥0∞: supremum of ‖k‖₊ for all k ∈ spectrum 𝕜 a
• NormedRing.algEquivComplexOfComplete: Gelfand-Mazur theorem For a complex Banach division algebra, the natural algebraMap ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a

Main statements

• spectrum.isOpen_resolventSet: the resolvent set is open.
• spectrum.isClosed: the spectrum is closed.
• spectrum.subset_closedBall_norm: the spectrum is a subset of closed disk of radius equal to the norm.
• spectrum.isCompact: the spectrum is compact.
• spectrum.spectralRadius_le_nnnorm: the spectral radius is bounded above by the norm.
• spectrum.hasDerivAt_resolvent: the resolvent function is differentiable on the resolvent set.
• spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius: Gelfand's formula for the spectral radius in Banach algebras over ℂ.
• spectrum.nonempty: the spectrum of any element in a complex Banach algebra is nonempty.

TODO

• compute all derivatives of resolvent a.

noncomputable def spectralRadius (𝕜 : Type u_1) {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) : ENNReal

The spectral radius is the supremum of the nnnorm (‖·‖₊) of elements in the spectrum, coerced into an element of ℝ≥0∞. Note that it is possible for spectrum 𝕜 a = ∅. In this case, spectralRadius a = 0. It is also possible that spectrum 𝕜 a be unbounded (though not for Banach algebras, see spectrum.isBounded, below). In this case, spectralRadius a = ∞.

Equations

• spectralRadius 𝕜 a = ⨆ k ∈ spectrum 𝕜 a, ↑‖k‖₊

@[simp]

theorem spectrum.SpectralRadius.of_subsingleton {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [Subsingleton A] (a : A) : spectralRadius 𝕜 a = 0

@[simp]

theorem spectrum.spectralRadius_zero {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] : spectralRadius 𝕜 0 = 0

theorem spectrum.mem_resolventSet_of_spectralRadius_lt {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] {a : A} {k : 𝕜} (h : spectralRadius 𝕜 a < ↑‖k‖₊) : k ∈ resolventSet 𝕜 a

theorem spectrum.isOpen_resolventSet {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : IsOpen (resolventSet 𝕜 a)

theorem spectrum.isClosed {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : IsClosed (spectrum 𝕜 a)

theorem spectrum.mem_resolventSet_of_norm_lt_mul {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜} (h : ‖a‖ * ‖1‖ < ‖k‖) : k ∈ resolventSet 𝕜 a

theorem spectrum.mem_resolventSet_of_norm_lt {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] {a : A} {k : 𝕜} (h : ‖a‖ < ‖k‖) : k ∈ resolventSet 𝕜 a

theorem spectrum.norm_le_norm_mul_of_mem {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜} (hk : k ∈ spectrum 𝕜 a) : ‖k‖ ≤ ‖a‖ * ‖1‖

theorem spectrum.norm_le_norm_of_mem {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] {a : A} {k : 𝕜} (hk : k ∈ spectrum 𝕜 a) : ‖k‖ ≤ ‖a‖

theorem spectrum.subset_closedBall_norm_mul {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : spectrum 𝕜 a ⊆ Metric.closedBall 0 (‖a‖ * ‖1‖)

theorem spectrum.subset_closedBall_norm {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] (a : A) : spectrum 𝕜 a ⊆ Metric.closedBall 0 ‖a‖

theorem spectrum.isBounded {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : Bornology.IsBounded (spectrum 𝕜 a)

theorem spectrum.isCompact {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] (a : A) : IsCompact (spectrum 𝕜 a)

instance spectrum.instCompactSpace {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] (a : A) : CompactSpace ↑(spectrum 𝕜 a)

instance spectrum.instCompactSpaceNNReal {A : Type u_3} [NormedRing A] [NormedAlgebra ℝ A] (a : A) [CompactSpace ↑(spectrum ℝ a)] : CompactSpace ↑(spectrum NNReal a)

theorem quasispectrum.isCompact {𝕜 : Type u_1} [NormedField 𝕜] {B : Type u_3} [NonUnitalNormedRing B] [NormedSpace 𝕜 B] [CompleteSpace B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [ProperSpace 𝕜] (a : B) : IsCompact (quasispectrum 𝕜 a)

instance quasispectrum.instCompactSpace {𝕜 : Type u_1} [NormedField 𝕜] {B : Type u_3} [NonUnitalNormedRing B] [NormedSpace 𝕜 B] [CompleteSpace B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [ProperSpace 𝕜] (a : B) : CompactSpace ↑(quasispectrum 𝕜 a)

instance quasispectrum.instCompactSpaceNNReal {B : Type u_3} [NonUnitalNormedRing B] [NormedSpace ℝ B] [IsScalarTower ℝ B B] [SMulCommClass ℝ B B] (a : B) [CompactSpace ↑(quasispectrum ℝ a)] : CompactSpace ↑(quasispectrum NNReal a)

theorem spectrum.le_nnnorm_of_mem {A : Type u_3} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [NormOneClass A] {a : A} {r : NNReal} (hr : r ∈ spectrum NNReal a) : r ≤ ‖a‖₊

theorem spectrum.coe_le_norm_of_mem {A : Type u_3} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [NormOneClass A] {a : A} {r : NNReal} (hr : r ∈ spectrum NNReal a) : ↑r ≤ ‖a‖

theorem spectrum.spectralRadius_le_nnnorm {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] (a : A) : spectralRadius 𝕜 a ≤ ↑‖a‖₊

theorem spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] {a : A} (ha : (spectrum 𝕜 a).Nonempty) : ∃ k ∈ spectrum 𝕜 a, ↑‖k‖₊ = spectralRadius 𝕜 a

theorem spectrum.spectralRadius_lt_of_forall_lt_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] {a : A} (ha : (spectrum 𝕜 a).Nonempty) {r : NNReal} (hr : ∀ k ∈ spectrum 𝕜 a, ‖k‖₊ < r) : spectralRadius 𝕜 a < ↑r

theorem spectrum.spectralRadius_le_pow_nnnorm_pow_one_div (𝕜 : Type u_1) {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) (n : ℕ) : spectralRadius 𝕜 a ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))

theorem spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div (𝕜 : Type u_1) {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : spectralRadius 𝕜 a ≤ Filter.liminf (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop

theorem spectrum.hasDerivAt_resolvent {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a) : HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

theorem spectrum.eventually_isUnit_resolvent {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : ∀ᶠ (z : 𝕜) in Bornology.cobounded 𝕜, IsUnit (resolvent a z)

theorem spectrum.resolvent_isBigO_inv {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : resolvent a =O[Bornology.cobounded 𝕜] Inv.inv

theorem spectrum.resolvent_tendsto_cobounded {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : Filter.Tendsto (resolvent a) (Bornology.cobounded 𝕜) (nhds 0)

theorem spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul (𝕜 : Type u_1) {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] (a : A) : HasFPowerSeriesOnBall (fun (z : 𝕜) => Ring.inverse (1 - z • a)) (fun (n : ℕ) => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 (↑‖a‖₊)⁻¹

In a Banach algebra A over a nontrivially normed field 𝕜, for any a : A the power series with coefficients a ^ n represents the function (1 - z • a)⁻¹ in a disk of radius ‖a‖₊⁻¹.

theorem spectrum.isUnit_one_sub_smul_of_lt_inv_radius {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] {a : A} {z : 𝕜} (h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹) : IsUnit (1 - z • a)

theorem spectrum.differentiableOn_inverse_one_sub_smul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {r : NNReal} (hr : ↑r < (spectralRadius 𝕜 a)⁻¹) : DifferentiableOn 𝕜 (fun (z : 𝕜) => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)

In a Banach algebra A over 𝕜, for a : A the function fun z ↦ (1 - z • a)⁻¹ is differentiable on any closed ball centered at zero of radius r < (spectralRadius 𝕜 a)⁻¹.

theorem spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.limsup (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop ≤ spectralRadius ℂ a

The limsup relationship for the spectral radius used to prove spectrum.gelfand_formula.

theorem spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.Tendsto (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))

Gelfand's formula: Given an element a : A of a complex Banach algebra, the spectralRadius of a is the limit of the sequence ‖a ^ n‖₊ ^ (1 / n).

theorem spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.Tendsto (fun (n : ℕ) => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) Filter.atTop (nhds (spectralRadius ℂ a))

Gelfand's formula: Given an element a : A of a complex Banach algebra, the spectralRadius of a is the limit of the sequence ‖a ^ n‖₊ ^ (1 / n).

theorem spectrum.nonempty {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) : (spectrum ℂ a).Nonempty

In a (nontrivial) complex Banach algebra, every element has nonempty spectrum.

theorem spectrum.exists_nnnorm_eq_spectralRadius {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) : ∃ z ∈ spectrum ℂ a, ↑‖z‖₊ = spectralRadius ℂ a

In a complex Banach algebra, the spectral radius is always attained by some element of the spectrum.

theorem spectrum.spectralRadius_lt_of_forall_lt {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) {r : NNReal} (hr : ∀ z ∈ spectrum ℂ a, ‖z‖₊ < r) : spectralRadius ℂ a < ↑r

In a complex Banach algebra, if every element of the spectrum has norm strictly less than r : ℝ≥0, then the spectral radius is also strictly less than r.

theorem spectrum.map_polynomial_aeval {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) (p : Polynomial ℂ) : spectrum ℂ ((Polynomial.aeval a) p) = (fun (k : ℂ) => Polynomial.eval k p) '' spectrum ℂ a

The spectral mapping theorem for polynomials in a Banach algebra over ℂ.

theorem spectrum.map_pow {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) (n : ℕ) : spectrum ℂ (a ^ n) = (fun (x : ℂ) => x ^ n) '' spectrum ℂ a

A specialization of the spectral mapping theorem for polynomials in a Banach algebra over ℂ to monic monomials.

theorem spectrum.algebraMap_eq_of_mem {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) {a : A} {z : ℂ} (h : z ∈ spectrum ℂ a) : (algebraMap ℂ A) z = a

noncomputable def NormedRing.algEquivComplexOfComplete {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) [CompleteSpace A] : ℂ ≃ₐ[ℂ] A

Gelfand-Mazur theorem: For a complex Banach division algebra, the natural algebraMap ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a. In addition, algebraMap_isometry guarantees this map is an isometry.

Note: because NormedDivisionRing requires the field norm_mul' : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖, we don't use this type class and instead opt for a NormedRing in which the nonzero elements are precisely the units. This allows for the application of this isomorphism in broader contexts, e.g., to the quotient of a complex Banach algebra by a maximal ideal. In the case when A is actually a NormedDivisionRing, one may fill in the argument hA with the lemma isUnit_iff_ne_zero.

Equations

• NormedRing.algEquivComplexOfComplete hA = { toFun := ⇑(algebraMap ℂ A), invFun := fun (a : A) => ⋯.some, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem NormedRing.algEquivComplexOfComplete_apply {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) [CompleteSpace A] (a : ℂ) : (NormedRing.algEquivComplexOfComplete hA) a = (algebraMap ℂ A) a

@[simp]

theorem NormedRing.algEquivComplexOfComplete_symm_apply {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) [CompleteSpace A] (a : A) : (NormedRing.algEquivComplexOfComplete hA).symm a = ⋯.some

theorem spectrum.exp_mem_exp {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) {z : 𝕜} (hz : z ∈ spectrum 𝕜 a) : NormedSpace.exp 𝕜 z ∈ spectrum 𝕜 (NormedSpace.exp 𝕜 a)

For 𝕜 = ℝ or 𝕜 = ℂ, exp 𝕜 maps the spectrum of a into the spectrum of exp 𝕜 a.

@[instance 100]

instance AlgHom.instContinuousLinearMapClassOfAlgHomClass {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] : ContinuousLinearMapClass F 𝕜 A 𝕜

def AlgHom.toContinuousLinearMap {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜

An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).

Equations

• φ.toContinuousLinearMap = { toLinearMap := φ.toLinearMap, cont := ⋯ }

@[simp]

theorem AlgHom.coe_toContinuousLinearMap {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (φ : A →ₐ[𝕜] 𝕜) : ⇑φ.toContinuousLinearMap = ⇑φ

theorem AlgHom.norm_apply_le_self_mul_norm_one {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F) (a : A) : ‖f a‖ ≤ ‖a‖ * ‖1‖

theorem AlgHom.norm_apply_le_self {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F) (a : A) : ‖f a‖ ≤ ‖a‖

@[simp]

theorem AlgHom.toContinuousLinearMap_norm {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] (φ : A →ₐ[𝕜] 𝕜) : ‖φ.toContinuousLinearMap‖ = 1

def WeakDual.CharacterSpace.equivAlgHom {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [CompleteSpace A] [NormedAlgebra 𝕜 A] : ↑(WeakDual.characterSpace 𝕜 A) ≃ (A →ₐ[𝕜] 𝕜)

The equivalence between characters and algebra homomorphisms into the base field.

Equations

• WeakDual.CharacterSpace.equivAlgHom = { toFun := WeakDual.CharacterSpace.toAlgHom, invFun := fun (f : A →ₐ[𝕜] 𝕜) => ⟨f.toContinuousLinearMap, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem WeakDual.CharacterSpace.equivAlgHom_coe {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [CompleteSpace A] [NormedAlgebra 𝕜 A] (f : ↑(WeakDual.characterSpace 𝕜 A)) : ⇑(WeakDual.CharacterSpace.equivAlgHom f) = ⇑f

@[simp]

theorem WeakDual.CharacterSpace.equivAlgHom_symm_coe {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [CompleteSpace A] [NormedAlgebra 𝕜 A] (f : A →ₐ[𝕜] 𝕜) : ⇑(WeakDual.CharacterSpace.equivAlgHom.symm f) = ⇑f

theorem Subalgebra.isUnit_of_isUnit_val_of_eventually {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] {l : Filter ↥S} {a : ↥S} (ha : IsUnit ↑a) (hla : l ≤ nhds a) (hl : ∀ᶠ (x : ↥S) in l, IsUnit x) (hl' : l.NeBot) : IsUnit a

Let S be a closed subalgebra of a Banach algebra A. If a : S is invertible in A, and for all x : S sufficiently close to a within some filter l, x is invertible in S, then a is invertible in S as well.

theorem Subalgebra.frontier_spectrum {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) : frontier (spectrum 𝕜 x) ⊆ spectrum 𝕜 ↑x

If S : Subalgebra 𝕜 A is a closed subalgebra of a Banach algebra A, then for any x : S, the boundary of the spectrum of x relative to S is a subset of the spectrum of ↑x : A relative to A.

theorem Subalgebra.frontier_subset_frontier {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) : frontier (spectrum 𝕜 x) ⊆ frontier (spectrum 𝕜 ↑x)

If S is a closed subalgebra of a Banach algebra A, then for any x : S, the boundary of the spectrum of x relative to S is a subset of the boundary of the spectrum of ↑x : A relative to A.

theorem Subalgebra.spectrum_sUnion_connectedComponentIn {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) : spectrum 𝕜 x = spectrum 𝕜 ↑x ∪ ⋃ z ∈ spectrum 𝕜 x \ spectrum 𝕜 ↑x, connectedComponentIn (spectrum 𝕜 ↑x)ᶜ z

If S is a closed subalgebra of a Banach algebra A, then for any x : S, the spectrum of x is the spectrum of ↑x : A along with the connected components of the complement of the spectrum of ↑x : A which contain an element of the spectrum of x : S.

theorem Subalgebra.spectrum_isBounded_connectedComponentIn {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) {z : 𝕜} (hz : z ∈ spectrum 𝕜 x) : Bornology.IsBounded (connectedComponentIn (spectrum 𝕜 ↑x)ᶜ z)

Let S be a closed subalgebra of a Banach algebra A, and let x : S. If z is in the spectrum of x, then the connected component of z in the complement of the spectrum of ↑x : A is bounded (or else z actually belongs to the spectrum of ↑x : A).

theorem Subalgebra.spectrum_eq_of_isPreconnected_compl {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 A] [SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) (h : IsPreconnected (spectrum 𝕜 ↑x)ᶜ) : spectrum 𝕜 x = spectrum 𝕜 ↑x

Let S be a closed subalgebra of a Banach algebra A. If for x : S the complement of the spectrum of ↑x : A is connected, then spectrum 𝕜 x = spectrum 𝕜 (x : A).

theorem SpectrumRestricts.spectralRadius_eq {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} {A : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedRing A] [NormedAlgebra 𝕜₁ A] [NormedAlgebra 𝕜₂ A] [NormedAlgebra 𝕜₁ 𝕜₂] [IsScalarTower 𝕜₁ 𝕜₂ A] {f : 𝕜₂ → 𝕜₁} {a : A} (h : SpectrumRestricts a f) : spectralRadius 𝕜₁ a = spectralRadius 𝕜₂ a

If 𝕜₁ is a normed field contained as subfield of a larger normed field 𝕜₂, and if a : A is an element whose 𝕜₂ spectrum restricts to 𝕜₁, then the spectral radii over each scalar field coincide.

theorem SpectrumRestricts.nnreal_iff {A : Type u_3} [Ring A] [Algebra ℝ A] {a : A} : SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x

theorem SpectrumRestricts.nnreal_of_nonneg {A : Type u_4} [Ring A] [PartialOrder A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) : SpectrumRestricts a ⇑ContinuousMap.realToNNReal

theorem SpectrumRestricts.real_iff {A : Type u_3} [Ring A] [Algebra ℂ A] {a : A} : SpectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = ↑x.re

theorem SpectrumRestricts.nnreal_le_iff {A : Type u_3} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} : (∀ x ∈ spectrum NNReal a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, ↑r ≤ x

theorem SpectrumRestricts.nnreal_lt_iff {A : Type u_3} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} : (∀ x ∈ spectrum NNReal a, r < x) ↔ ∀ x ∈ spectrum ℝ a, ↑r < x

theorem SpectrumRestricts.le_nnreal_iff {A : Type u_3} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} : (∀ x ∈ spectrum NNReal a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ ↑r

theorem SpectrumRestricts.lt_nnreal_iff {A : Type u_3} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} : (∀ x ∈ spectrum NNReal a, x < r) ↔ ∀ x ∈ spectrum ℝ a, x < ↑r

theorem SpectrumRestricts.nnreal_iff_spectralRadius_le {A : Type u_3} [Ring A] [Algebra ℝ A] {a : A} {t : NNReal} (ht : spectralRadius ℝ a ≤ ↑t) : SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

theorem NNReal.spectralRadius_mem_spectrum {A : Type u_4} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty) (ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) : (spectralRadius ℝ a).toNNReal ∈ spectrum NNReal a

theorem Real.spectralRadius_mem_spectrum {A : Type u_4} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty) (ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) : (spectralRadius ℝ a).toReal ∈ spectrum ℝ a

theorem Real.spectralRadius_mem_spectrum_or {A : Type u_4} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty) : (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

theorem QuasispectrumRestricts.compactSpace {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] {a : A} (f : C(S, R)) (h : QuasispectrumRestricts a ⇑f) [h_cpct : CompactSpace ↑(quasispectrum S a)] : CompactSpace ↑(quasispectrum R a)

theorem QuasispectrumRestricts.nnreal_iff {A : Type u_3} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ quasispectrum ℝ a, 0 ≤ x

theorem QuasispectrumRestricts.nnreal_of_nonneg {A : Type u_3} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal

theorem QuasispectrumRestricts.real_iff {A : Type u_3} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] {a : A} : QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ quasispectrum ℂ a, x = ↑x.re

theorem QuasispectrumRestricts.le_nnreal_iff {A : Type u_3} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} (ha : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} : (∀ x ∈ quasispectrum NNReal a, x ≤ r) ↔ ∀ x ∈ quasispectrum ℝ a, x ≤ ↑r

theorem QuasispectrumRestricts.lt_nnreal_iff {A : Type u_3} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} (ha : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} : (∀ x ∈ quasispectrum NNReal a, x < r) ↔ ∀ x ∈ quasispectrum ℝ a, x < ↑r

theorem coe_mem_spectrum_real_of_nonneg {A : Type u_3} [Ring A] [PartialOrder A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] {a : A} {x : NNReal} (ha : 0 ≤ a := by cfc_tac) : ↑x ∈ spectrum ℝ a ↔ x ∈ spectrum NNReal a