StarAlgHom.nnnorm_apply_le
theorem StarAlgHom.nnnorm_apply_le :
∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A]
[inst_2 : CompleteSpace A] [inst_3 : StarRing A] [inst_4 : CstarRing A] [inst_5 : NormedRing B]
[inst_6 : NormedAlgebra ℂ B] [inst_7 : CompleteSpace B] [inst_8 : StarRing B] [inst_9 : CstarRing B]
[inst_10 : FunLike F A B] [inst_11 : AlgHomClass F ℂ A B] [inst_12 : StarAlgHomClass F ℂ A B] (φ : F) (a : A),
‖φ a‖₊ ≤ ‖a‖₊
This theorem states that for any star algebra homomorphism (represented by φ) between two complex C*-algebras (A and B), the norm of the homomorphism applied to an element from A (‖φ a‖₊) is less than or equal to the norm of that element in A (‖a‖₊). The algebras A and B are assumed to have a structure of a normed ring, a normed algebra over the complex numbers, a complete metric space, a star ring, and a C* ring.
More concisely: For any star algebra homomorphism φ between two complex C*-algebras A and B, ‖φ(a)‖₊ ≤ ‖a‖₊ holds for all elements a in A.
|
IsSelfAdjoint.mem_spectrum_eq_re
theorem IsSelfAdjoint.mem_spectrum_eq_re :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] [inst_3 : StarRing A]
[inst_4 : CstarRing A] [inst_5 : StarModule ℂ A] {a : A},
IsSelfAdjoint a → ∀ {z : ℂ}, z ∈ spectrum ℂ a → z = ↑z.re
The theorem `IsSelfAdjoint.mem_spectrum_eq_re` states that for any self-adjoint element `a` of a C*-algebra `A` over the complex numbers, any complex number `z` that lies in the spectrum of `a` must be equal to its real part. Here, a C*-algebra is a type of normed algebra that also has a *-operation (star operation), a complex conjugation-like operation. 'Self-adjoint' means that the element is equal to its own *-conjugate. The 'spectrum' of an element in an algebra is the set of scalars for which the difference between the scalar multiplication of the unit element and the algebra element is not invertible. In simpler terms, this theorem is saying that the eigenvalues (spectrum) of a self-adjoint operator in a C*-algebra are real numbers.
More concisely: A self-adjoint element in a C*-algebra has real spectrum.
|
selfAdjoint.mem_spectrum_eq_re
theorem selfAdjoint.mem_spectrum_eq_re :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] [inst_3 : StarRing A]
[inst_4 : CstarRing A] [inst_5 : StarModule ℂ A] (a : ↥(selfAdjoint A)) {z : ℂ}, z ∈ spectrum ℂ ↑a → z = ↑z.re
The theorem `selfAdjoint.mem_spectrum_eq_re` states that for any element `a` of the self-adjoint elements of a normed ring `A` with complex number algebra, any complex number `z` that belongs to the spectrum of `a` is equal to its real part. This means that any element of the spectrum of a self-adjoint element is a real number. The normed ring `A` is also assumed to be a complete space, a star ring, a C* ring, and a star module over the field of complex numbers.
More concisely: For any self-adjoint element `a` in the complex normed ring `A`, every complex number `z` in the spectrum of `a` equals its real part.
|
IsSelfAdjoint.val_re_map_spectrum
theorem IsSelfAdjoint.val_re_map_spectrum :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] [inst_3 : StarRing A]
[inst_4 : CstarRing A] [inst_5 : StarModule ℂ A] {a : A},
IsSelfAdjoint a → spectrum ℂ a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ a
The theorem `IsSelfAdjoint.val_re_map_spectrum` states that for any element `a` of a certain type `A`, where `A` is a Normed Ring, a Normed Algebra over the complex numbers, a Complete Space, a Star Ring, a C* Ring, and a Star Module over the complex numbers, if `a` is self-adjoint, then the spectrum of `a` in the complex numbers is equal to the image of the spectrum of `a` in the complex numbers under the composition of the map `Complex.ofReal'` and the real part function `Complex.re`.
In simpler terms, it says that for a certain mathematical structure `A`, if an element `a` in `A` is self-adjoint, then the set of complex numbers for which `a` has a certain algebraic property (`a`'s spectrum) is the same as the set of real parts of complex numbers which also have that property for `a`, converted back into complex numbers.
More concisely: If `a` is a self-adjoint element in a Normed Ring, C* Ring, Star Ring, or Star Module over the complex numbers, then the spectrum of `a` is equal to the set of complex numbers obtained by applying the real part function and the complex Numbers embedding to the spectrum of `a`.
|
StarAlgHom.norm_apply_le
theorem StarAlgHom.norm_apply_le :
∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A]
[inst_2 : CompleteSpace A] [inst_3 : StarRing A] [inst_4 : CstarRing A] [inst_5 : NormedRing B]
[inst_6 : NormedAlgebra ℂ B] [inst_7 : CompleteSpace B] [inst_8 : StarRing B] [inst_9 : CstarRing B]
[inst_10 : FunLike F A B] [inst_11 : AlgHomClass F ℂ A B] [inst_12 : StarAlgHomClass F ℂ A B] (φ : F) (a : A),
‖φ a‖ ≤ ‖a‖
The theorem `StarAlgHom.norm_apply_le` states that, for any types `F`, `A`, and `B`, given that `A` and `B` are normed rings, normed ℂ-algebras, complete spaces, star rings, and C⋆-rings; `F` is a function-like from `A` to `B`; and `F` is an algebra homomorphism and a star algebra homomorphism, then for any function `φ` of type `F` and any element `a` of type `A`, the norm of the result of applying `φ` to `a` is less than or equal to the norm of `a`. In other words, a star algebra homomorphism of complex C⋆-algebras is norm contractive.
More concisely: Given two normed rings and C⋆-algebras `A` and `B`, a complete space `F` that is a function-like, algebra homomorphism, and star algebra homomorphism from `A` to `B`, the norm of `F(a)` is less than or equal to the norm of `a` for all `a` in `A`.
|
selfAdjoint.val_re_map_spectrum
theorem selfAdjoint.val_re_map_spectrum :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] [inst_3 : StarRing A]
[inst_4 : CstarRing A] [inst_5 : StarModule ℂ A] (a : ↥(selfAdjoint A)),
spectrum ℂ ↑a = Complex.ofReal' ∘ Complex.re '' spectrum ℂ ↑a
The theorem `selfAdjoint.val_re_map_spectrum` states that for any self-adjoint A, which is an element of a C*-ring A, a complete space, a normed ring, and a normed algebra over the complex numbers with a compatible star-module structure, the spectrum of A in the complex numbers is equal to the set obtained by taking the real part of the spectrum of A in the complex numbers and then embedding these real numbers back into the complex numbers. In other words, the spectrum of a self-adjoint operator consists only of real numbers, which is a known result in functional analysis.
More concisely: The spectrum of a self-adjoint element in a C*-algebra is equal to the set of its real eigenvalues.
|