Documentation

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Instances of the continuous functional calculus #

Main theorems #

Tags #

continuous functional calculus, normal, selfadjoint

Pull back a non-unital instance from a unital one on the unitization #

noncomputable def cfcₙAux {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : AProp} {p₁ : Unitization 𝕜 AProp} (hp₁ : ∀ {x : A}, p₁ x p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 p₁] :

This is an auxiliary definition used for constructing an instance of the non-unital continuous functional calculus given a instance of the unital one on the unitization.

This is the natural non-unital star homomorphism obtained from the chain

calc
  C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] C(σₙ 𝕜 a, 𝕜) := ContinuousMapZero.toContinuousMapHom
  _             ≃⋆[𝕜] C(σ 𝕜 (↑a : A⁺¹), 𝕜) := Homeomorph.compStarAlgEquiv'
  _             →⋆ₐ[𝕜] A⁺¹ := cfcHom

This range of this map is contained in the range of (↑) : A → A⁺¹ (see cfcₙAux_mem_range_inr), and so we may restrict it to A to get the necessary homomorphism for the non-unital continuous functional calculus.

Equations
Instances For
    theorem cfcₙAux_id {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : AProp} {p₁ : Unitization 𝕜 AProp} (hp₁ : ∀ {x : A}, p₁ x p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 p₁] :
    (cfcₙAux a ha) (ContinuousMapZero.id ) = a
    theorem closedEmbedding_cfcₙAux {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : AProp} {p₁ : Unitization 𝕜 AProp} (hp₁ : ∀ {x : A}, p₁ x p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 p₁] :
    theorem spec_cfcₙAux {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : AProp} {p₁ : Unitization 𝕜 AProp} (hp₁ : ∀ {x : A}, p₁ x p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 p₁] (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) :
    spectrum 𝕜 ((cfcₙAux a ha) f) = Set.range f
    theorem cfcₙAux_mem_range_inr {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : AProp} {p₁ : Unitization 𝕜 AProp} (hp₁ : ∀ {x : A}, p₁ x p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 p₁] [CompleteSpace A] (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) :
    theorem RCLike.nonUnitalContinuousFunctionalCalculus {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : AProp} {p₁ : Unitization 𝕜 AProp} (hp₁ : ∀ {x : A}, p₁ x p x) [ContinuousFunctionalCalculus 𝕜 p₁] [CompleteSpace A] [CStarRing A] :

    Continuous functional calculus for normal elements #

    Continuous functional calculus for selfadjoint elements #

    An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its quasispectrum is contained in .

    Alias of the forward direction of isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts.


    An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its quasispectrum is contained in .

    A normal element whose -quasispectrum is contained in is selfadjoint.

    An element in a C⋆-algebra is selfadjoint if and only if it is normal and its spectrum is contained in .

    A normal element whose -spectrum is contained in is selfadjoint.

    theorem IsSelfAdjoint.spectrum_nonempty {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra A] [ContinuousFunctionalCalculus IsSelfAdjoint] [Nontrivial A] {a : A} (ha : IsSelfAdjoint a) :
    (spectrum a).Nonempty

    Continuous functional calculus for nonnegative elements #

    theorem NNReal.spectrum_nonempty {A : Type u_2} [Ring A] [StarRing A] [PartialOrder A] [TopologicalSpace A] [Algebra NNReal A] [ContinuousFunctionalCalculus NNReal fun (x : A) => 0 x] [Nontrivial A] {a : A} (ha : 0 a) :
    (spectrum NNReal a).Nonempty

    The spectrum of a nonnegative element is nonnegative #

    theorem spectrum_star_mul_self_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra A] [StarModule A] {b : A} (x : ) :
    x spectrum (star b * b)0 x
    @[reducible]

    The partial order on a unital C⋆-algebra defined by x ≤ y if and only if y - x is selfadjoint and has nonnegative spectrum.

    This is not declared as an instance because one may already have a partial order with better definitional properties. However, it can be useful to invoke this as an instance in proofs.

    Equations
    Instances For

      The restriction of a continuous functional calculus is equal to the original one #

      theorem cfc_real_eq_complex {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra A] [ContinuousFunctionalCalculus IsStarNormal] [UniqueContinuousFunctionalCalculus A] {a : A} (f : ) (ha : autoParam (IsSelfAdjoint a) _auto✝) :
      cfc f a = cfc (fun (x : ) => (f x.re)) a
      theorem cfc_nnreal_eq_real {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra A] [TopologicalRing A] [ContinuousFunctionalCalculus IsSelfAdjoint] [ContinuousFunctionalCalculus NNReal fun (x : A) => 0 x] [UniqueContinuousFunctionalCalculus A] [NonnegSpectrumClass A] {a : A} (f : NNRealNNReal) (ha : autoParam (0 a) _auto✝) :
      cfc f a = cfc (fun (x : ) => (f x.toNNReal)) a