mathlib documentation

analysis.normed_space.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 [normed_field 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [star_module 𝕜 E].

TODO #

@[class]
structure normed_star_group (E : Type u_1) [semi_normed_group E] [star_add_monoid E] :
Prop

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

Instances of this typeclass
@[simp]

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

Equations

The star map in a normed star group is an isometry

@[class]
structure cstar_ring (E : Type u_4) [non_unital_normed_ring E] [star_ring E] :
Prop

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]

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

@[simp]
theorem cstar_ring.norm_one {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] :
@[protected, instance]
theorem cstar_ring.norm_coe_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] (U : (unitary E)) :
@[simp]
theorem cstar_ring.norm_of_mem_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] {U : E} (hU : U unitary E) :
@[simp]
theorem cstar_ring.norm_coe_unitary_mul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (U : (unitary E)) (A : E) :
@[simp]
theorem cstar_ring.norm_unitary_smul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (U : (unitary E)) (A : E) :
theorem cstar_ring.norm_mem_unitary_mul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {U : E} (A : E) (hU : U unitary E) :
@[simp]
theorem cstar_ring.norm_mul_coe_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (A : E) (U : (unitary E)) :
theorem cstar_ring.norm_mul_mem_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (A : E) {U : E} (hU : U unitary E) :
theorem nnnorm_pow_two_pow_of_self_adjoint {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {x : E} (hx : x self_adjoint E) (n : ) :
x ^ 2 ^ n∥₊ = x∥₊ ^ 2 ^ n
theorem self_adjoint.nnnorm_pow_two_pow {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (x : (self_adjoint E)) (n : ) :
x ^ 2 ^ n∥₊ = x∥₊ ^ 2 ^ n
def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [normed_star_group E] [module 𝕜 E] [star_module 𝕜 E] :

star bundled as a linear isometric equivalence

Equations
@[simp]
theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [normed_star_group E] [module 𝕜 E] [star_module 𝕜 E] :
theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [normed_star_group E] [module 𝕜 E] [star_module 𝕜 E] {x : E} :