LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional
theorem LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : FiniteDimensional 𝕜 E] [_i : Nontrivial E] {T : E →ₗ[𝕜] E},
T.IsSymmetric → Module.End.HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
The theorem states that for any scalar field `𝕜` that behaves like the real or complex numbers (denoted by `RCLike 𝕜`), and any finite-dimensional, non-trivial vector space `E` over `𝕜` with an inner product, if we have a symmetric linear operator `T` on `E`, then the supremum of the Rayleigh quotient of `T` is an eigenvalue of `T`. In mathematical terms, this means that there exists a non-zero vector in the vector space such that when it is transformed by the operator, the output is a scalar multiple of the original vector. The scalar in this case is the supremum of the Rayleigh quotient, which is represented by `⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2`. The Rayleigh quotient is a function that measures how much a given vector is stretched or compressed by the operator `T`, and its supremum gives the maximum possible stretching or compression ratio.
More concisely: For any finite-dimensional, non-trivial inner product space over a scalar field behaving like the real or complex numbers, a symmetric linear operator has an eigenvalue equal to the supremum of its Rayleigh quotient.
|
IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn
theorem IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
IsSelfAdjoint T →
∀ {x₀ : E},
x₀ ≠ 0 →
IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
Module.End.HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀
This theorem states that for any self-adjoint linear operator `T` acting on a complete inner product space over a field `𝕜`, if a point `x₀` on a sphere (centered at the origin with radius equal to the norm of `x₀`) is a local extremum of the Rayleigh quotient of `T`, then `x₀` is an eigenvector of `T`. The Rayleigh quotient of `T` at `x₀` is then the corresponding eigenvalue. Note that `x₀` cannot be the zero vector.
More concisely: If a self-adjoint linear operator `T` on a complete inner product space over a field `𝕜` has a point `x₀` on the sphere of radius equal to `‖x₀‖` an eigenvector with corresponding eigenvalue equal to the Rayleigh quotient of `T` at `x₀`, then `x₀` is an eigenvector of `T`.
|
LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional
theorem LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : FiniteDimensional 𝕜 E] [_i : Nontrivial E] {T : E →ₗ[𝕜] E},
T.IsSymmetric → Module.End.HasEigenvalue T ↑(⨅ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
The theorem `LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional` states that for any scalar field `𝕜` satisfying the `RCLike` class, a given nontrivial finite-dimensional inner product space `E` over `𝕜`, and a symmetric linear operator `T` on `E`, the infimum of the Rayleigh quotient of `T` is an eigenvalue of `T`. The Rayleigh quotient is calculated as the real part of the inner product of `T` applied to a vector `x` and the original vector `x`, all divided by the squared norm of `x`. This infimum is taken over all vectors `x` in the space. The theorem essentially captures the concept that the smallest Rayleigh quotient of a symmetric operator corresponds to an eigenvalue of the operator.
More concisely: For any nontrivial finite-dimensional inner product space over a scalar field with a symmetric linear operator, the infimum of the Rayleigh quotient over all vectors is an eigenvalue.
|
IsSelfAdjoint.hasEigenvector_of_isMinOn
theorem IsSelfAdjoint.hasEigenvector_of_isMinOn :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
IsSelfAdjoint T →
∀ {x₀ : E},
x₀ ≠ 0 →
IsMinOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
Module.End.HasEigenvector (↑T) (↑(⨅ x, T.rayleighQuotient ↑x)) x₀
The theorem `IsSelfAdjoint.hasEigenvector_of_isMinOn` states that for a self-adjoint operator `T` on an inner product space over a ring-like structure `𝕜` and a complete normed add-commutative group `E`, any point `x₀` on the sphere centred at origin with radius equal to the norm of `x₀` that minimizes the Rayleigh quotient of `T` is an eigenvector of `T`. Moreover, the corresponding eigenvalue is the global infimum of the Rayleigh quotient of `T`.
More concisely: A self-adjoint operator T on an inner product space over a ring-like structure 𝕜 and complete normed add-commutative group E with radius-minimizing point x₀ on its sphere having smallest Rayleigh quotient is an eigenvector of T with the corresponding eigenvalue equal to the global minimum of the Rayleigh quotient.
|
IsSelfAdjoint.hasEigenvector_of_isMaxOn
theorem IsSelfAdjoint.hasEigenvector_of_isMaxOn :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
[inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
IsSelfAdjoint T →
∀ {x₀ : E},
x₀ ≠ 0 →
IsMaxOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
Module.End.HasEigenvector (↑T) (↑(⨆ x, T.rayleighQuotient ↑x)) x₀
The theorem `IsSelfAdjoint.hasEigenvector_of_isMaxOn` states that for a self-adjoint operator `T` on a complete inner product space over a field that is R-like (like the real or complex numbers), any point `x₀` that is not zero and maximizes the Rayleigh quotient of `T` on a sphere centered at the origin is an eigenvector of `T`. Furthermore, the corresponding eigenvalue is equal to the global supremum of the Rayleigh quotient. Here, `T.reApplyInnerSelf` is the function that maps a point to the inner product of `T` applied to the point and the point itself, which effectively realizes the Rayleigh quotient. The metric sphere `Metric.sphere 0 ‖x₀‖` is the set of all points at a distance `‖x₀‖` from the origin.
More concisely: For a self-adjoint operator T on a complete inner product space over an R-like field, if x₀ is a non-zero point maximizing T.reApplyInnerSelf on the sphere centered at the origin with radius ‖x₀‖, then x₀ is an eigenvector of T with eigenvalue equal to the supremum of T.reApplyInnerSelf over the sphere.
|