Documentation

Mathlib.Analysis.Normed.Algebra.Spectrum

The spectrum of elements in a complete normed algebra #

This file contains the basic theory for the resolvent and spectrum of a Banach algebra. Theorems specific to complex Banach algebras, such as Gelfand's formula can be found in Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean.

Main definitions #

Main statements #

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

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
Instances For
    @[simp]
    theorem spectrum.SpectralRadius.of_subsingleton {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] [Subsingleton A] (a : A) :
    spectralRadius 𝕜 a = 0
    @[simp]
    theorem spectrum.spectralRadius_zero {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] :
    spectralRadius 𝕜 0 = 0
    @[simp]
    theorem spectrum.spectralRadius_one {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] :
    spectralRadius 𝕜 1 = 1
    theorem spectrum.mem_resolventSet_of_spectralRadius_lt {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] {a : A} {k : 𝕜} (h : spectralRadius 𝕜 a < k‖₊) :
    k resolventSet 𝕜 a
    theorem spectrum.spectralRadius_pow_le {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (n : ) (hn : n 0) :
    spectralRadius 𝕜 a ^ n spectralRadius 𝕜 (a ^ n)
    theorem spectrum.spectralRadius_pow_le' {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] [Nontrivial A] (a : A) (n : ) :
    spectralRadius 𝕜 a ^ n spectralRadius 𝕜 (a ^ n)
    theorem spectrum.isOpen_resolventSet {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) :
    @[simp]
    theorem spectrum.isClosed {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : 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) :
    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) :
    @[simp]
    theorem spectrum.isBounded {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) :
    @[simp]
    theorem spectrum.isCompact {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] (a : A) :
    instance spectrum.instCompactSpace {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] (a : A) :
    @[simp]
    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) :
    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) :
    theorem spectrum.spectralRadius_le_nnnorm {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] (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) :
    kspectrum 𝕜 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 : kspectrum 𝕜 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.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.exp_mem_exp {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) {z : 𝕜} (hz : z spectrum 𝕜 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 𝕜] :
    def AlgHom.toContinuousLinearMap {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (φ : A →ₐ[𝕜] 𝕜) :
    StrongDual 𝕜 A

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

    Equations
    Instances For
      @[simp]
      theorem AlgHom.coe_toContinuousLinearMap {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (φ : A →ₐ[𝕜] 𝕜) :
      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) :
      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) :
      def WeakDual.CharacterSpace.equivAlgHom {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [CompleteSpace A] [NormedAlgebra 𝕜 A] :
      (characterSpace 𝕜 A) (A →ₐ[𝕜] 𝕜)

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

      Equations
      Instances For
        @[simp]
        theorem WeakDual.CharacterSpace.equivAlgHom_coe {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [CompleteSpace A] [NormedAlgebra 𝕜 A] (f : (characterSpace 𝕜 A)) :
        (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 →ₐ[𝕜] 𝕜) :
        (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) :

        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 zspectrum 𝕜 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) :

        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.real_iff {A : Type u_3} [Ring A] [Algebra A] {a : A} :
        theorem SpectrumRestricts.nnreal_le_iff {A : Type u_3} [Ring A] [Algebra A] {a : A} (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : NNReal} :
        (∀ xspectrum NNReal a, r x) xspectrum 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} :
        (∀ xspectrum NNReal a, r < x) xspectrum 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} :
        (∀ xspectrum NNReal a, x r) xspectrum 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} :
        (∀ xspectrum NNReal a, x < r) xspectrum a, x < r
        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)] :
        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) :