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.

Main definitions #

Main statements #

TODO #

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 𝕜] [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) :
    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) :
    theorem spectrum.isBounded {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) :
    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) :
    Equations
    • =
    Equations
    • =
    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) :
    Equations
    • =
    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.hasDerivAt_resolvent {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜} (hk : k resolventSet 𝕜 a) :
    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.hasFPowerSeriesOnBall_inverse_one_sub_smul (𝕜 : Type u_1) {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace 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).

    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.

    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 : zspectrum a, z‖₊ < 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.

    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
    @[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) :
    noncomputable def NormedRing.algEquivComplexOfComplete {A : Type u_2} [NormedRing A] [NormedAlgebra A] (hA : ∀ {a : A}, IsUnit a a 0) [CompleteSpace 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
    • One or more equations did not get rendered due to their size.
    Instances For
      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 𝕜] :
      Equations
      • =
      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 = let __src := φ.toLinearMap; { toLinearMap := __src, cont := }
      Instances For
        @[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) :
        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) :
        @[simp]
        theorem AlgHom.toContinuousLinearMap_norm {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] (φ : A →ₐ[𝕜] 𝕜) :
        φ.toContinuousLinearMap = 1

        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 := }
        Instances For
          @[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 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} :
          SpectrumRestricts a Complex.reCLM xspectrum a, x = x.re
          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)] :