LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply
theorem LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{T : E →L[𝕜] E}, T.IsSymmetric → ∀ (x : E), ↑(T.reApplyInnerSelf x) = ⟪T x, x⟫_𝕜
This theorem states that for any symmetric operator `T` on a normed add-commutative group `E` over a field `𝕜` with an inner product space structure, the function that maps `x` to the inner product of `T x` and `x`, denoted by ⟪T x, x⟫_𝕜, is real-valued. That is, when applied to any element `x` of `E`, the real part of the application of `T` to `x` with itself (i.e., `T.reApplyInnerSelf x`) equals to the inner product of `T x` and `x`.
More concisely: For any symmetric operator T on a normed add-commutative group E over a field 𝕜 with an inner product space structure, the real part of the inner product of T x and x equals the inner product of T x and x for all x in E. (i.e., Re(∫(Tx, x)𝕜) = ∫(Tx, x)𝕜 for all x in E)
|
LinearMap.isSymmetric_iff_sesqForm
theorem LinearMap.isSymmetric_iff_sesqForm :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(T : E →ₗ[𝕜] E), T.IsSymmetric ↔ sesqFormOfInner.IsSelfAdjoint T
The theorem `LinearMap.isSymmetric_iff_sesqForm` states that for any linear operator `T` on an inner product space over a field `𝕜`, `T` is symmetric if and only if it is self-adjoint with respect to the sesquilinear form given by the inner product. Here, an operator is considered symmetric if it is equal to its adjoint, and a sesquilinear form is a complex-valued function that is linear in one argument and conjugate-linear in the other. This theorem establishes a connection between these two notions of symmetry for operators on an inner product space.
More concisely: A linear operator T on an inner product space is symmetric if and only if it is self-adjoint with respect to the given sesquilinear form (inner product).
|
LinearMap.IsSymmetric.inner_map_polarization
theorem LinearMap.IsSymmetric.inner_map_polarization :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{T : E →ₗ[𝕜] E},
T.IsSymmetric →
∀ (x y : E),
⟪T x, y⟫_𝕜 =
(⟪T (x + y), x + y⟫_𝕜 - ⟪T (x - y), x - y⟫_𝕜 - RCLike.I * ⟪T (x + RCLike.I • y), x + RCLike.I • y⟫_𝕜 +
RCLike.I * ⟪T (x - RCLike.I • y), x - RCLike.I • y⟫_𝕜) /
4
This theorem is a statement of the polarization identity for symmetric linear maps. It applies to a field '𝕜' that satisfies the `RCLike` typeclass, and a normed add commutative group 'E' that also has an inner product space structure over '𝕜'. Given a symmetric linear map 'T' from 'E' to 'E', the theorem states that for all vectors 'x' and 'y' in 'E', the inner product of 'T x' and 'y' can be expressed as a certain combination of four other inner products. Specifically, it is equal to one-fourth of the difference between the inner products of 'T' applied to 'x + y' and 'x - y', minus the product of the imaginary unit 'I' and the inner product of 'T' applied to 'x + Iy', plus the product of 'I' and the inner product of 'T' applied to 'x - Iy'.
More concisely: For a symmetric linear map T from a normed add commutative group E with an inner product over a field 𝕜, the inner product of T(x) and y equals one-quarter(Ip(T(x+y))-Ip(T(x-y))+i(Ip(T(x+iy))-Ip(T(x-iy)))), where i is the imaginary unit.
|
LinearMap.IsSymmetric.continuous
theorem LinearMap.IsSymmetric.continuous :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : CompleteSpace E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → Continuous ⇑T
This theorem is known as the Hellinger-Toeplitz theorem. It states that for any symmetric linear operator `T` defined on a complete inner product space `E` over a scalar field `𝕜`, `T` is automatically continuous. In mathematical terms, if `E` is a complete space and `T` is a symmetric operator, then `T` is continuous. This theorem plays a fundamental role in the functional analysis, specifically in the study of Hilbert spaces.
More concisely: A symmetric linear operator on a complete inner product space is continuous.
|
LinearMap.IsSymmetric.inner_map_self_eq_zero
theorem LinearMap.IsSymmetric.inner_map_self_eq_zero :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{T : E →ₗ[𝕜] E}, T.IsSymmetric → ((∀ (x : E), ⟪T x, x⟫_𝕜 = 0) ↔ T = 0)
The theorem `LinearMap.IsSymmetric.inner_map_self_eq_zero` states that for every field `𝕜` and every inner product space `E` over `𝕜`, a symmetric linear map `T` from `E` to `E` is zero if and only if the inner product of `T x` and `x` equals zero for every element `x` of `E`. There is a complex version of the theorem which does not require the symmetric assumption, named `inner_map_self_eq_zero`.
More concisely: A linear map T from an inner product space E over a field 𝕜 is symmetric if and only if T x = 0 for all x in E if and only if the inner product of x and T x equals zero for all x in E.
|
LinearMap.IsSymmetric.restrict_invariant
theorem LinearMap.IsSymmetric.restrict_invariant :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ {V : Submodule 𝕜 E} (hV : ∀ v ∈ V, T v ∈ V), (T.restrict hV).IsSymmetric
This theorem states that if a symmetric linear operator preserves a submodule, then its restriction to that submodule is also symmetric. Here, 𝕜 is a type representing the field over which the vector space is defined, E is the type of the vector space, T is the symmetric linear operator, and V is the submodule. The operator T is said to preserve the submodule V if for every vector v in V, the result of applying T to v is also in V. The restriction of T to V is the operator that behaves like T, but is only defined on V. This theorem asserts that if T is symmetric and preserves V, then this restriction of T to V is also symmetric.
More concisely: If a symmetric linear operator T preserves a submodule V, then the restriction of T to V is also a symmetric linear operator.
|
LinearMap.isSymmetric_iff_inner_map_self_real
theorem LinearMap.isSymmetric_iff_inner_map_self_real :
∀ {V : Type u_6} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V),
T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
This theorem states that a linear operator `T` on a complex inner product space `V` is symmetric if and only if the inner product of `T v` and `v` is a real number for all `v` in `V`. In other words, if for every vector in the space, the complex conjugate of the inner product of the vector and its image under `T` equals the original inner product, then `T` is a symmetric operator.
More concisely: A linear operator T on a complex inner product space V is symmetric if and only if the inner product of T v and v is real for all v in V. (Equivalently, the inner product of T v and v is conjugate-symmetric: (T v | v) = (v | T v)).
|