LinearPMap.adjoint_isFormalAdjoint
theorem LinearPMap.adjoint_isFormalAdjoint :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
{T : E →ₗ.[𝕜] F}, Dense ↑T.domain → ∀ [inst_5 : CompleteSpace E], T.adjoint.IsFormalAdjoint T
This theorem, referred to as the fundamental property of the adjoint, states that for any type 𝕜, any normed additive commutative group E, any inner product space over 𝕜 E, any normed additive commutative group F, any inner product space over 𝕜 F, and any linear map T from E to F, if T's domain is dense in E (meaning that every point in E belongs to the closure of the domain of T), then under the additional condition that E is a complete space, the adjoint of T is a formal adjoint of T.
More concisely: If E is a complete normed additive commutative group with a dense domain, and T is a linear map from the inner product space over a field 𝕜, E to the inner product space over 𝕜, F, then the adjoint of T exists and is the formal adjoint of T.
|
IsSelfAdjoint.dense_domain
theorem IsSelfAdjoint.dense_domain :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : CompleteSpace E] {A : E →ₗ.[𝕜] E}, IsSelfAdjoint A → Dense ↑A.domain
This theorem states that every self-adjoint linear partial map (`LinearPMap`) has a dense domain. In the context of this theorem, a self-adjoint element is an element that is equivalent to its conjugate transpose ('star'), and a set is said to be dense in a topological space if every point belongs to its closure. While the adjoint is defined without the assumption of a dense domain, the selection of the "junk" value entails that a linear partial map can't be self-adjoint if its domain isn't dense. Here, the domain refers to the set of all possible inputs for the linear partial map, and dense means that every point in the topological space comes arbitrarily close to some point in the domain. This theorem is applicable to any normed add-commutative group and inner product space over any type that behaves like real or complex numbers.
More concisely: Every self-adjoint linear partial map on a dense domain in a normed add-commutative group or inner product space is densely defined.
|
LinearPMap.IsFormalAdjoint.le_adjoint
theorem LinearPMap.IsFormalAdjoint.le_adjoint :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
{S : F →ₗ.[𝕜] E}, Dense ↑T.domain → ∀ [inst_5 : CompleteSpace E], T.IsFormalAdjoint S → S ≤ T.adjoint
This theorem states that for an arbitrary field `𝕜` and two inner product spaces `E` and `F` over `𝕜`, given a linear map `T` from `E` to `F` and another linear map `S` from `F` to `E`, if the domain of `T` is dense and `E` is a complete space, then if `T` is a formal adjoint of `S`, `S` is less than or equal to the adjoint of `T`. In other words, the adjoint of a linear map contains all its formal adjoints if the map's domain is dense in the topological space and the space is complete.
More concisely: If `𝕜` is an arbitrary field, `E` and `F` are inner product spaces over `𝕜`, `T: E → F` is a linear map with dense domain and `E` is complete, `S: F → E` is the formal adjoint of `T`, then `S ≤ T*` (the adjoint of `T`).
|