LinearMap.eq_adjoint_iff
theorem LinearMap.eq_adjoint_iff :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : FiniteDimensional π E] [inst_6 : FiniteDimensional π F] (A : E ββ[π] F) (B : F ββ[π] E),
A = LinearMap.adjoint B β β (x : E) (y : F), βͺA x, yβ«_π = βͺx, B yβ«_π
The theorem states that for a given pair of linear maps `A` and `B` between two finite-dimensional inner product spaces over a field `π`, the map `A` is the adjoint of `B` if and only if it satisfies the condition that the inner product of `A x` and `y` is equal to the inner product of `x` and `B y` for all vectors `x` in the space `E` and `y` in the space `F`. In other words, the adjoint is unique and is determined by this inner product property.
More concisely: The linear maps \(A : E \rightarrow F\) and \(B : F \rightarrow E\) are adjoints of each other if and only if \(\langle Ax, y \rangle = \langle x, By \rangle\) for all \(x \in E\) and \(y \in F\), where \(\langle \cdot, \cdot \rangle\) denotes the inner product.
|
LinearMap.isSymmetric_adjoint_mul_self
theorem LinearMap.isSymmetric_adjoint_mul_self :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
[inst_3 : FiniteDimensional π E] (T : E ββ[π] E), (LinearMap.adjoint T * T).IsSymmetric
This theorem states that the Gram operator, represented as the product of the adjoint of a linear map `T` and `T` itself, is always symmetric. This holds for any type `π`, which behaves like a real or complex number, and any type `E`, which is a normed additive commutative group over `π` and an inner product space. Moreover, this theorem assumes that the type `E` is a finite-dimensional vector space over `π`. The theorem applies for any linear map `T` from `E` to `E`.
More concisely: For any finite-dimensional normed additive commutative group `E` over a real or complex number field `π`, and any linear map `T` from `E` to `E`, the Gram operator `(T.adjoint T)` is symmetric.
|
LinearMap.adjoint_comp
theorem LinearMap.adjoint_comp :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace π E]
[inst_5 : InnerProductSpace π F] [inst_6 : InnerProductSpace π G] [inst_7 : FiniteDimensional π E]
[inst_8 : FiniteDimensional π F] [inst_9 : FiniteDimensional π G] (A : F ββ[π] G) (B : E ββ[π] F),
LinearMap.adjoint (A ββ B) = LinearMap.adjoint B ββ LinearMap.adjoint A
The theorem `LinearMap.adjoint_comp` states that for any division ring `π` and finite dimensional inner product spaces `E`, `F`, and `G`, the adjoint of the composition of two linear maps (operators) is the composition of the adjoints of the two linear maps but in reverse order. Specifically, if `A` is a linear map from `F` to `G` and `B` is a linear map from `E` to `F`, then the adjoint of the composition of `A` and `B` is equal to the composition of the adjoint of `B` and the adjoint of `A`. This is a key property of adjoints in the context of linear maps and inner product spaces.
More concisely: For any division rings π and finite dimensional inner product spaces E, F, and G, the adjoint of the composition of linear maps A : F β G and B : E β F is equal to the composition of the adjoints of B and A, that is, (A β B)βΊ = BβΊ β AβΊ.
|
IsSelfAdjoint.adjoint_conj
theorem IsSelfAdjoint.adjoint_conj :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {T : E βL[π] E},
IsSelfAdjoint T β β (S : F βL[π] E), IsSelfAdjoint ((ContinuousLinearMap.adjoint S).comp (T.comp S))
The theorem `IsSelfAdjoint.adjoint_conj` states that conjugating preserves the property of self-adjointness. More specifically, for all types π, E, and F, given certain conditions on π, E, and F like π being RCLike, E and F being NormedAddCommGroups and InnerProductSpaces, and E and F being CompleteSpaces, if a continuous linear map T from E to E is self-adjoint, then for any continuous linear map S from F to E, the composition of the adjoint of S and T composed with S is also self-adjoint.
More concisely: If T is a self-adjoint continuous linear map between two RCLike, NormedAddCommGroups and InnerProductSpaces E and F, and S is a continuous linear map from F to E, then the composition of S, the adjoint of S, and T is a self-adjoint linear map.
|
ContinuousLinearMap.eq_adjoint_iff
theorem ContinuousLinearMap.eq_adjoint_iff :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E βL[π] F) (B : F βL[π] E),
A = ContinuousLinearMap.adjoint B β β (x : E) (y : F), βͺA x, yβ«_π = βͺx, B yβ«_π
This theorem, named `ContinuousLinearMap.eq_adjoint_iff`, states that a continuous linear map `A` from type `E` to type `F` is the adjoint of another continuous linear map `B` from type `F` to type `E` if and only if the inner product of `A x` and `y` equals the inner product of `x` and `B y` for all `x` of type `E` and `y` of type `F`. Here, `π` represents the underlying field, `E` and `F` are normed groups equipped with an inner product, and `A` and `B` are continuous linear maps. This means that the adjoint is unique: if a map satisfies the adjoint condition, it must be the adjoint.
More concisely: A continuous linear map `A` from normed group `E` to normed group `F` equipped with inner products is the adjoint of another continuous linear map `B` if and only if they satisfy the condition `βx:E, βy:F, β©x, B yβͺ = β©A x, yβͺ`.
|
Matrix.toEuclideanLin_conjTranspose_eq_adjoint
theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint :
β {π : Type u_1} [inst : RCLike π] {m : Type u_5} {n : Type u_6} [inst_1 : Fintype m] [inst_2 : DecidableEq m]
[inst_3 : Fintype n] [inst_4 : DecidableEq n] (A : Matrix m n π),
Matrix.toEuclideanLin A.conjTranspose = LinearMap.adjoint (Matrix.toEuclideanLin A)
The theorem `Matrix.toEuclideanLin_conjTranspose_eq_adjoint` states that for any type `π` that behaves like a ring, two types `m` and `n` representing the dimensions of a matrix, and a matrix `A` with entries in `π` and dimensions `m` by `n`, the linear map corresponding to the conjugate transpose of `A` is equal to the adjoint of the linear map corresponding to `A`. In other words, converting a matrix's conjugate transpose to a linear map is the same as taking the adjoint of the linear map corresponding to the original matrix. The adjoint of a linear map is a concept from linear algebra that generalizes the notion of a matrix transpose, while the conjugate transpose of a matrix involves not only transposing the matrix but also taking the complex conjugate of each entry. This theorem thus provides a connection between these two operations in the context of matrices and linear maps.
More concisely: For any ring `π` and matrices `A` of dimensions `m` by `n` over `π`, the conjugate transpose of `A` as a linear map is equal to the adjoint of `A` as a linear map.
|
orthogonalProjection_isSelfAdjoint
theorem orthogonalProjection_isSelfAdjoint :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
[inst_3 : CompleteSpace E] (U : Submodule π E) [inst_4 : CompleteSpace β₯U],
IsSelfAdjoint (U.subtypeL.comp (orthogonalProjection U))
This theorem states that the orthogonal projection onto a complete subspace is self-adjoint. In mathematical terms, for any ring-like structure `π` and any normed additive commutative group `E` that also has an inner product space structure over `π`, if `E` and its submodule `U` are both complete spaces, then the composition of the subtype linear map of `U` and the orthogonal projection onto `U` is a self-adjoint operation. Being self-adjoint means that this composite operation is equal to its star operation, which is an operation that produces the complex conjugate transpose (or adjoint) of a mathematical object.
More concisely: Given a ring-like structure `π`, a normed additive commutative group `E` with an inner product space structure over `π`, and a complete subspace `U` of `E`, the orthogonal projection onto `U` is self-adjoint as a linear operator on `E`.
|
LinearMap.adjoint_inner_right
theorem LinearMap.adjoint_inner_right :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : FiniteDimensional π E] [inst_6 : FiniteDimensional π F] (A : E ββ[π] F) (x : E) (y : F),
βͺx, (LinearMap.adjoint A) yβ«_π = βͺA x, yβ«_π
The theorem `LinearMap.adjoint_inner_right` states that for any given types π, E, and F, where π behaves like a commutative ring with division, E and F are normed additive commutative groups, and both E and F are inner product spaces over π and also finite-dimensional over π, for any linear map A from E to F, and any elements x in E and y in F, the inner product of x with the adjoint of A applied to y over π is equal to the inner product of A applied to x with y over π.
More concisely: For any finite-dimensional linear map A between inner product spaces X and Y over a commutative ring with division π, the inner product of x in X with the adjoint of A applied to y in Y equals the inner product of A(x) in Y with y in X.
|
ContinuousLinearMap.adjoint_adjoint
theorem ContinuousLinearMap.adjoint_adjoint :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E βL[π] F),
ContinuousLinearMap.adjoint (ContinuousLinearMap.adjoint A) = A
This theorem states that the adjoint operation on continuous linear maps is involutive, meaning that applying it twice brings us back to the original map. More specifically, given any continuous linear map `A` between two complete normed additive commutative groups `E` and `F` equipped with an inner product over a ring `π`, the adjoint of the adjoint of `A` is equal to `A` itself.
More concisely: The adjoint of a continuous linear map between two complete normed additive commutative groups with an inner product over a ring is equal to its double adjoint.
|
LinearMap.re_inner_adjoint_mul_self_nonneg
theorem LinearMap.re_inner_adjoint_mul_self_nonneg :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
[inst_3 : FiniteDimensional π E] (T : E ββ[π] E) (x : E), 0 β€ RCLike.re βͺx, (LinearMap.adjoint T * T) xβ«_π
The theorem `LinearMap.re_inner_adjoint_mul_self_nonneg` states that for any semi-outParam type `π`, normed add commutative group `E`, when `π` has a `RCLike` instance, `E` is a inner product space over `π` and `E` is a finite dimensional vector space over `π`, the real part of the inner product of a vector `x` and the result of applying the linear map `T` and its adjoint on `x` in sequence, is always non-negative. In mathematical terms, for any vector `x` and linear operator `T`, 0 β€ Reβ¨x, Tβ T xβ©, where `Tβ ` represents the adjoint of `T`. This effectively means that the Gram operator `Tβ T` is a positive operator.
More concisely: For any semi-outParam type `π` with an RCLike instance, normed add commutative group `E` that is a finite dimensional inner product space over `π`, the real part of the inner product of a vector `x` and the product of a linear map `T` and its adjoint `Tβ `, is non-negative: Reβ¨x, Tβ T xβ© β₯ 0.
|
LinearMap.isSelfAdjoint_iff'
theorem LinearMap.isSelfAdjoint_iff' :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
[inst_3 : FiniteDimensional π E] {A : E ββ[π] E}, IsSelfAdjoint A β LinearMap.adjoint A = A
The theorem states that for every continuous linear operator `A` on a finite-dimensional inner product space `E` over a field `π` with certain properties (specifically, `π` is a ring with conjugation and `E` is a normed commutative additive group), `A` is self-adjoint if and only if `A` is equal to its adjoint. In mathematical terms, a linear operator is considered self-adjoint if it is equal to its adjoint, where the adjoint of a linear operator is typically defined as a transformation that relates the dot product of a vector with the operator's output to the dot product of the operator's input with a given vector.
More concisely: A continuous linear operator A on a finite-dimensional inner product space over a ring with conjugation is self-adjoint if and only if A = A^*, where A^* is the adjoint operator.
|
IsSelfAdjoint.conj_adjoint
theorem IsSelfAdjoint.conj_adjoint :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {T : E βL[π] E},
IsSelfAdjoint T β β (S : E βL[π] F), IsSelfAdjoint (S.comp (T.comp (ContinuousLinearMap.adjoint S)))
The theorem states that conjugating preserves the property of being self-adjoint. Specifically, if we are given some types π, E and F, which are assumed to have the structure of a normed additive commutative group, an inner product space, and a complete space, and we have a continuous linear map T from E to E that is self-adjoint, then for any continuous linear map S from E to F, the composition of S, T, and the adjoint of S is also self-adjoint.
More concisely: If T is a continuous, self-adjoint linear map between two normed, additive commutative groups and inner product spaces E and F, then the composition of T with any continuous linear map S from E to F and the adjoint of S is also a self-adjoint linear map.
|
Matrix.toLin_conjTranspose
theorem Matrix.toLin_conjTranspose :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F] {m : Type u_5}
{n : Type u_6} [inst_5 : Fintype m] [inst_6 : DecidableEq m] [inst_7 : Fintype n] [inst_8 : DecidableEq n]
[inst_9 : FiniteDimensional π E] [inst_10 : FiniteDimensional π F] (vβ : OrthonormalBasis n π E)
(vβ : OrthonormalBasis m π F) (A : Matrix m n π),
(Matrix.toLin vβ.toBasis vβ.toBasis) A.conjTranspose =
LinearMap.adjoint ((Matrix.toLin vβ.toBasis vβ.toBasis) A)
This theorem states that for any field `π`, normed additive commutative groups `E` and `F` that are inner product spaces over `π`, types `m` and `n` that have finite cardinality and decidable equality, and `E` and `F` that are finite dimensional over `π`, given an orthonormal basis `vβ` of `n` over `π` in `E` and an orthonormal basis `vβ` of `m` over `π` in `F`, and a matrix `A` of `m` by `n` over `π`, the linear map associated to the conjugate transpose of `A` with respect to the bases `vβ` and `vβ` is equal to the adjoint of the linear map associated to `A` with respect to the bases `vβ` and `vβ`. In simpler terms, the theorem establishes a relationship between the adjoint operation in the context of linear maps and the conjugate transpose operation in the context of matrices, under the condition of orthonormal bases.
More concisely: For any finite dimensional, inner product spaces E and F over a field π with orthonormal bases vβ in E and vβ in F, the conjugate transpose of the matrix representing a linear map A from F to E with respect to vβ and vβ is equal to the adjoint of A.
|
LinearMap.adjoint_adjoint
theorem LinearMap.adjoint_adjoint :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : FiniteDimensional π E] [inst_6 : FiniteDimensional π F] (A : E ββ[π] F),
LinearMap.adjoint (LinearMap.adjoint A) = A
The theorem `LinearMap.adjoint_adjoint` states that for every linear map `A` from a finite dimensional inner product space `E` to another finite dimensional inner product space `F` over a ring `π` that behaves like the complex numbers (as specified by the `RCLike π` instance), applying the "adjoint" operation twice to `A` results in `A` itself. This property is known as the "involutiveness" of the adjoint.
More concisely: For any finite dimensional linear map A between inner product spaces over a ring behaving like the complex numbers, A ^ T * A = A, where A ^ T is the adjoint of A.
|
IsSelfAdjoint.isSymmetric
theorem IsSelfAdjoint.isSymmetric :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
[inst_3 : CompleteSpace E] {A : E βL[π] E}, IsSelfAdjoint A β A.IsSymmetric
This theorem states that every self-adjoint operator on an inner product space is symmetric. Here, a self-adjoint operator is defined as an operator that is equal to its own adjoint (reflected across a specific kind of axis). The theorem applies to any type π with a ring-like structure (RCLike π), and to any type E that is a normed additive commutative group and an inner-product space over π. It also assumes that E is a complete space. The operator in question is a continuous linear map from E to E over the field π, denoted as A. If A is self-adjoint, then the theorem concludes that A is also symmetric.
More concisely: If A is a self-adjoint, continuous linear operator on a complete inner-product space E over a ring-like field π, then A is symmetric.
|
LinearMap.eq_adjoint_iff_basis
theorem LinearMap.eq_adjoint_iff_basis :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : FiniteDimensional π E] [inst_6 : FiniteDimensional π F] {ΞΉβ : Type u_5} {ΞΉβ : Type u_6}
(bβ : Basis ΞΉβ π E) (bβ : Basis ΞΉβ π F) (A : E ββ[π] F) (B : F ββ[π] E),
A = LinearMap.adjoint B β β (iβ : ΞΉβ) (iβ : ΞΉβ), βͺA (bβ iβ), bβ iββ«_π = βͺbβ iβ, B (bβ iβ)β«_π
This theorem, titled `LinearMap.eq_adjoint_iff_basis`, states that within a given inner product space, a linear map `A` is the adjoint of another linear map `B` if and only if it satisfies the equality `βͺA x, yβ« = βͺx, B yβ«` for all basis vectors `x` and `y`. Here, `βͺ , β«_π` denotes the inner product with respect to the division ring `π`, `E` and `F` are finite dimensional vector spaces over `π` with `bβ` and `bβ` as their respective bases, and `A` and `B` are linear maps between these vector spaces. The theorem asserts the uniqueness of the adjoint in the context of these vector spaces and linear maps.
More concisely: A linear map A is the adjoint of another linear map B in an inner product space if and only if they satisfy the condition that the inner product of A x and y equals the inner product of x and By for all basis vectors x and y.
|
LinearMap.adjoint_inner_left
theorem LinearMap.adjoint_inner_left :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace π E] [inst_4 : InnerProductSpace π F]
[inst_5 : FiniteDimensional π E] [inst_6 : FiniteDimensional π F] (A : E ββ[π] F) (x : E) (y : F),
βͺ(LinearMap.adjoint A) y, xβ«_π = βͺy, A xβ«_π
The theorem `LinearMap.adjoint_inner_left` describes the fundamental property of the adjoint of a linear map in the context of inner product spaces. For any division ring `π`, normed add-commutive groups `E` and `F`, and instances of inner product spaces over `π` for both `E` and `F`, which are also finite dimensional, and for any linear map `A` from `E` to `F`, and elements `x` in `E` and `y` in `F`, the inner product of `y` with the image of `x` under `A` is equal to the inner product of the image of `y` under the adjoint of `A` with `x`. In mathematical notation, this is saying that for all `x` in `E` and `y` in `F`, β¨(A* y), xβ© = β¨y, A xβ© where `A*` denotes the adjoint of `A`.
More concisely: For any linear map A between finite-dimensional inner product spaces E and F over a division ring, the inner product of y in F with Ax in E equals the inner product of Ay in F with x in E. (A\* denotes the adjoint of A.)
|
ContinuousLinearMap.isSelfAdjoint_iff'
theorem ContinuousLinearMap.isSelfAdjoint_iff' :
β {π : Type u_1} {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace π E]
[inst_3 : CompleteSpace E] {A : E βL[π] E}, IsSelfAdjoint A β ContinuousLinearMap.adjoint A = A
This theorem states that for any continuous linear operator `A` on a complete inner product space `E` over the field `π`, `A` is self-adjoint if and only if it is equal to its adjoint. In the context of this theorem, a field `π` is said to be RCLike (presumably meaning it behaves like the real or complex numbers), and `E` is a normed additive commutative group. Being self-adjoint means that an operator is equal to its own adjoint, or equivalently, its 'star'.
More concisely: A continuous linear operator A on a complete inner product space E over a RCLike field is self-adjoint if and only if A = A*.
|