LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.InnerProductSpace.Spectrum

`LinearMap.IsSymmetric.orthogonalFamily_eigenspaces` theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → OrthogonalFamily 𝕜 (fun μ => ↥(Module.End.eigenspace T μ)) fun μ => (Module.End.eigenspace T μ).subtypeₗᵢ The theorem `LinearMap.IsSymmetric.orthogonalFamily_eigenspaces` asserts that for a self-adjoint operator `T` on an inner product space `E` over a type `𝕜` that behaves like a real or complex field (denoted by `RCLike 𝕜`), the eigenspaces of `T` are mutually orthogonal. In other words, if `T` is a self-adjoint operator, then for any different eigenvalues `μ` and `ν`, the inner product of any vector from the eigenspace of `μ` and any vector from the eigenspace of `ν` is zero. This is a fundamental result in the theory of self-adjoint operators in inner product spaces. More concisely: For a self-adjoint operator T on an inner product space E over a real or complex field, the eigenspaces of distinct eigenvalues are orthogonal.
`LinearMap.IsSymmetric.direct_sum_isInternal` theorem LinearMap.IsSymmetric.direct_sum_isInternal : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ [inst_3 : FiniteDimensional 𝕜 E], DirectSum.IsInternal fun μ => Module.End.eigenspace T (↑T μ) This theorem states that for a self-adjoint operator `T` on a finite-dimensional inner product space `E` over a field `𝕜`, the eigenspaces of `T` provide an internal direct sum decomposition of `E`. This means that `E` can be expressed as a direct sum of its eigenspaces. In mathematical notation, given a self-adjoint operator `T`, we have `E = ⊕ μ eigenspace(T, μ)`, where `μ` ranges over all eigenvalues of `T`. The `DirectSum.IsInternal` function is a way of saying that a space is the direct sum of a family of subspaces. More concisely: For a self-adjoint operator T on a finite-dimensional inner product space E, the eigenspaces of T form an internal direct sum decomposition of E.
`LinearMap.IsSymmetric.orthogonalFamily_eigenspaces'` theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → OrthogonalFamily 𝕜 (fun μ => ↥(Module.End.eigenspace T (↑T μ))) fun μ => (Module.End.eigenspace T (↑T μ)).subtypeₗᵢ This theorem states that for any type `𝕜` that behaves like a real or complex number (i.e., `𝕜` is `RCLike`), and any type `E` that forms a normed additive commutative group and an inner product space over `𝕜`, if we have a symmetric linear map `T` from `E` to `E` (i.e., `⟪T x, y⟫ = ⟪x, T y⟫` for all `x`, `y` in `E`), then the family of eigenspaces of `T` is orthogonal. Here, an eigenspace of `T` for a scalar `μ` consists of all vectors `x` such that `T x = μ • x`. In more detail, the theorem establishes that for each scalar `μ`, the elements of the eigenspace (which is a submodule of `E`) can be treated as a linearly independent set under the inner product (i.e., they form an orthogonal family), where the inner product on the eigenspace is induced by the natural embedding of the eigenspace into `E`. More concisely: For any `RCLike` type `𝕜`, normed additive commutative group and inner product space `E` over `𝕜`, and symmetric linear map `T` from `E` to `E`, the eigenspaces of `T` are orthogonal under the induced inner product.
`LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot` theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ [inst_3 : FiniteDimensional 𝕜 E], (⨆ μ, Module.End.eigenspace T μ).orthogonal = ⊥ This theorem states that for a self-adjoint operator `T` on a finite-dimensional inner product space `E` over a field `𝕜` that supports ordered rings, the orthogonal complement of the union of `T`'s eigenspaces is trivial, i.e., it only contains the zero vector. In other words, every vector in `E` is either in an eigenspace of `T` or is orthogonal to an eigenspace of `T`. More concisely: For a self-adjoint operator T on a finite-dimensional inner product space E over a field supporting ordered rings, the orthogonal complement of the union of T's eigenspaces is the zero subspace.
`LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant` theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ ⦃v : E⦄, v ∈ (⨆ μ, Module.End.eigenspace T μ).orthogonal → T v ∈ (⨆ μ, Module.End.eigenspace T μ).orthogonal This theorem states that for a self-adjoint operator `T` on an inner product space `E` over a field `𝕜`, the orthogonal complement of the union of all the eigenspaces of `T` is an invariant subspace of the operator `T`. In other words, if a vector `v` is orthogonal to all eigenspaces of `T`, then the image of `v` under the operator `T` is also orthogonal to all the eigenspaces of `T`. More concisely: The orthogonal complement of the sum of all eigenspaces of a self-adjoint operator `T` on an inner product space `E` is an invariant subspace of `T`.
`LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace` theorem LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (μ : 𝕜), ∀ v ∈ (Module.End.eigenspace T μ).orthogonal, T v ∈ (Module.End.eigenspace T μ).orthogonal The theorem `LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace` states that for any self-adjoint operator `T` on an inner product space over a field `𝕜`, and for any scalar `μ`, if a vector `v` belongs to the orthogonal complement of the eigenspace of `T` corresponding to `μ`, then the image of `v` under `T` also belongs to the orthogonal complement of the same eigenspace. In other words, a self-adjoint operator preserves the orthogonal complements of its eigenspaces. More concisely: For any self-adjoint linear operator T over an inner product space and scalar μ, if v belongs to the orthogonal complement of T's eigenspace with eigenvalue μ, then T(v) also belongs to the orthogonal complement of that eigenspace.
`LinearMap.IsSymmetric.conj_eigenvalue_eq_self` theorem LinearMap.IsSymmetric.conj_eigenvalue_eq_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ {μ : 𝕜}, Module.End.HasEigenvalue T μ → (starRingEnd 𝕜) μ = μ This theorem states that the eigenvalues of a self-adjoint operator are real numbers. Specifically, for any type `𝕜` that behaves like a ring of complex numbers, any normed additive commutative group `E`, and any inner product space formed over `𝕜` and `E`, if you have a linear map `T` from `E` to `E` that is symmetric, then for any eigenvalue `μ` of `T`, the complex conjugate of `μ` (represented by `(starRingEnd 𝕜) μ`) is equal to `μ` itself. This property is characteristic of real numbers within the complex plane, hence the statement that the eigenvalues of a self-adjoint operator are real. More concisely: The eigenvalues of a self-adjoint linear operator over a complex ring are equal to their complex conjugates.
`LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces` theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (μ : 𝕜), Module.End.eigenspace (T.restrict ⋯) μ = ⊥ The theorem `LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces` states that for any scalar `μ`, the eigenspace of the restriction of a symmetric linear operator (also known as a self-adjoint operator in the context of inner product spaces) `T` to its orthogonal complement is trivial. In other words, there are no eigenvectors (apart from the zero vector) in the orthogonal complement of the eigenspaces of a symmetric operator, hence it has no eigenvalues. More concisely: For a symmetric linear operator T, its eigenspaces have trivial orthogonal complements in the sense that there are no non-zero eigenvectors in the orthogonal complement of any eigenspace.
`LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply` theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) (v : E) (i : Fin n), (hT.eigenvectorBasis hn).repr (T v) i = ↑(hT.eigenvalues hn i) * (hT.eigenvectorBasis hn).repr v i The Diagonalization Theorem, also known as the Spectral Theorem, in its second version states that a self-adjoint operator `T` on a finite-dimensional inner product space `E`, behaves in a diagonal manner with respect to the identification of `E` with Euclidean space, induced by an orthonormal basis of eigenvectors of `T`. Precisely, for any vector `v` in `E` and any integer `i` within the finite rank `n` of `E`, the `i`-th coordinate of the image of `v` under `T` with respect to this basis, equals the product of the `i`-th eigenvalue of `T` and the `i`-th coordinate of `v` itself. More concisely: A self-adjoint operator T on a finite-dimensional inner product space aligns with the diagonal matrix of its eigenvalues when represented with respect to an orthonormal basis of eigenvectors.