Documentation

Mathlib.Analysis.NormedSpace.Star.Basic

Normed star rings and algebras #

A normed star group is a normed group with a compatible star which is isometric.

A C⋆-ring is a normed star group that is also a ring and that verifies the stronger condition ‖x⋆ * x‖ = ‖x‖^2 for all x. If a C⋆-ring is also a star algebra, then it is a C⋆-algebra.

To get a C⋆-algebra E over field 𝕜, use [NormedField 𝕜] [StarRing 𝕜] [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra 𝕜 E] [StarModule 𝕜 E].

TODO #

source
class NormedStarGroup (E : Type u_1) [SeminormedAddCommGroup E] [StarAddMonoid E] :
Prop

A normed star group is a normed group with a compatible star which is isometric.

Instances
    source
    @[simp]
    theorem NormedStarGroup.norm_star {E : Type u_1} [SeminormedAddCommGroup E] [StarAddMonoid E] [self : NormedStarGroup E] (x : E) :
    ‖star x‖ = ‖x‖
    source
    @[simp]
    theorem nnnorm_star {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] (x : E) :
    ‖star x‖₊ = ‖x‖₊
    source
    def starNormedAddGroupHom {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] :
    NormedAddGroupHom E E

    The star map in a normed star group is a normed group homomorphism.

    Equations
    • starNormedAddGroupHom = let __src := starAddEquiv; { toFun := __src.toFun, map_add' := ⋯, bound' := ⋯ }
    Instances For
      source
      theorem star_isometry {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] :
      Isometry star

      The star map in a normed star group is an isometry

      source
      @[instance 100]
      instance NormedStarGroup.to_continuousStar {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] :
      ContinuousStar E
      Equations
      • ⋯ = ⋯
      source
      instance RingHomIsometric.starRingEnd {E : Type u_2} [NormedCommRing E] [StarRing E] [NormedStarGroup E] :
      RingHomIsometric (starRingEnd E)
      Equations
      • ⋯ = ⋯
      source
      class CstarRing (E : Type u_4) [NonUnitalNormedRing E] [StarRing E] :
      Prop

      A C*-ring is a normed star ring that satisfies the stronger condition ‖x⋆ * x‖ = ‖x‖^2 for every x.

      Instances
        source
        theorem CstarRing.norm_star_mul_self {E : Type u_4} [NonUnitalNormedRing E] [StarRing E] [self : CstarRing E] {x : E} :
        ‖star x * x‖ = ‖x‖ * ‖x‖
        source
        instance instCstarRingReal :
        CstarRing ℝ
        Equations
        source
        @[instance 100]
        instance CstarRing.to_normedStarGroup {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] :
        NormedStarGroup E

        In a C*-ring, star preserves the norm.

        Equations
        • ⋯ = ⋯
        source
        theorem CstarRing.norm_self_mul_star {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] {x : E} :
        ‖x * star x‖ = ‖x‖ * ‖x‖
        source
        theorem CstarRing.norm_star_mul_self' {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] {x : E} :
        ‖star x * x‖ = ‖star x‖ * ‖x‖
        source
        theorem CstarRing.nnnorm_self_mul_star {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] {x : E} :
        ‖x * star x‖₊ = ‖x‖₊ * ‖x‖₊
        source
        theorem CstarRing.nnnorm_star_mul_self {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] {x : E} :
        ‖star x * x‖₊ = ‖x‖₊ * ‖x‖₊
        source
        @[simp]
        theorem CstarRing.star_mul_self_eq_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] (x : E) :
        star x * x = 0 ↔ x = 0
        source
        theorem CstarRing.star_mul_self_ne_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] (x : E) :
        star x * x ≠ 0 ↔ x ≠ 0
        source
        @[simp]
        theorem CstarRing.mul_star_self_eq_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] (x : E) :
        x * star x = 0 ↔ x = 0
        source
        theorem CstarRing.mul_star_self_ne_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CstarRing E] (x : E) :
        x * star x ≠ 0 ↔ x ≠ 0
        source
        instance Pi.starRing' {ι : Type u_4} {R : ι → Type u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] :
        StarRing ((i : ι) → R i)

        This instance exists to short circuit type class resolution because of problems with inference involving Π-types.

        Equations
        • Pi.starRing' = inferInstance
        source
        instance Prod.cstarRing {R₁ : Type u_5} {R₂ : Type u_6} [NonUnitalNormedRing R₁] [StarRing R₁] [CstarRing R₁] [NonUnitalNormedRing R₂] [StarRing R₂] [CstarRing R₂] :
        CstarRing (R₁ × R₂)
        Equations
        • ⋯ = ⋯
        source
        instance Pi.cstarRing {ι : Type u_4} {R : ι → Type u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] [Fintype ι] [∀ (i : ι), CstarRing (R i)] :
        CstarRing ((i : ι) → R i)
        Equations
        • ⋯ = ⋯
        source
        instance Pi.cstarRing' {ι : Type u_4} {R₁ : Type u_5} [NonUnitalNormedRing R₁] [StarRing R₁] [CstarRing R₁] [Fintype ι] :
        CstarRing (ι → R₁)
        Equations
        • ⋯ = ⋯
        source
        @[simp]
        theorem CstarRing.norm_one {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [Nontrivial E] :
        ‖1‖ = 1
        source
        @[instance 100]
        instance CstarRing.instNormOneClassOfNontrivial {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [Nontrivial E] :
        NormOneClass E
        Equations
        • ⋯ = ⋯
        source
        theorem CstarRing.norm_coe_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [Nontrivial E] (U : ↥(unitary E)) :
        ‖↑U‖ = 1
        source
        @[simp]
        theorem CstarRing.norm_of_mem_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [Nontrivial E] {U : E} (hU : U ∈ unitary E) :
        ‖U‖ = 1
        source
        @[simp]
        theorem CstarRing.norm_coe_unitary_mul {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] (U : ↥(unitary E)) (A : E) :
        ‖↑U * A‖ = ‖A‖
        source
        @[simp]
        theorem CstarRing.norm_unitary_smul {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] (U : ↥(unitary E)) (A : E) :
        ‖U • A‖ = ‖A‖
        source
        theorem CstarRing.norm_mem_unitary_mul {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] {U : E} (A : E) (hU : U ∈ unitary E) :
        ‖U * A‖ = ‖A‖
        source
        @[simp]
        theorem CstarRing.norm_mul_coe_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] (A : E) (U : ↥(unitary E)) :
        ‖A * ↑U‖ = ‖A‖
        source
        theorem CstarRing.norm_mul_mem_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] (A : E) {U : E} (hU : U ∈ unitary E) :
        ‖A * U‖ = ‖A‖
        source
        theorem IsSelfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] {x : E} (hx : IsSelfAdjoint x) (n : ℕ) :
        ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
        source
        theorem selfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] (x : ↥(selfAdjoint E)) (n : ℕ) :
        ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
        source
        def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] :
        E ≃ₗᵢ⋆[𝕜] E

        star bundled as a linear isometric equivalence

        Equations
        • starₗᵢ 𝕜 = let __src := starAddEquiv; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }
        Instances For
          source
          @[simp]
          theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] :
          ⇑(starₗᵢ 𝕜) = star
          source
          theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] {x : E} :
          (starₗᵢ 𝕜) x = star x
          source
          @[simp]
          theorem starₗᵢ_toContinuousLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] :
          (starₗᵢ 𝕜).toContinuousLinearEquiv = starL 𝕜
          source
          instance StarSubalgebra.toNormedAlgebra {𝕜 : Type u_4} {A : Type u_5} [NormedField 𝕜] [StarRing 𝕜] [SeminormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) :
          NormedAlgebra 𝕜 ↥S
          Equations
          source
          instance StarSubalgebra.to_cstarRing {R : Type u_4} {A : Type u_5} [CommRing R] [StarRing R] [NormedRing A] [StarRing A] [CstarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :
          CstarRing ↥S
          Equations
          • ⋯ = ⋯