Finite-dimensional inner product spaces

In this file, we prove some results in finite-dimensional inner product spaces.

Notation

This file uses the local notation P _ for orthogonal_projection _ and ↥P _ for the extended orthogonal projection orthogonal_projection' _.

We let $V$ be an inner product space over $\mathbb{k}$.

theorem Submodule.invariantUnder_iff_ortho_adjoint_invariant {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (U : Submodule 𝕜 V) (T : V →ₗ[𝕜] V) : U.InvariantUnder T ↔ Uᗮ.InvariantUnder (LinearMap.adjoint T)

$U$ is $T$-invariant if and only if $U^\bot$ is $T^*$ invariant

theorem Submodule.invariantUnder_iff_ortho_adjoint_invariant' {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (U : Submodule 𝕜 V) [CompleteSpace V] [hU : CompleteSpace ↥U] (T : V →L[𝕜] V) : U.InvariantUnder ↑T ↔ Uᗮ.InvariantUnder ↑(ContinuousLinearMap.adjoint T)

theorem IsSelfAdjoint.submodule_invariant_iff_ortho_submodule_invariant {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (U : Submodule 𝕜 V) (T : V →ₗ[𝕜] V) (h : IsSelfAdjoint T) : U.InvariantUnder T ↔ Uᗮ.InvariantUnder T

$T$ is self adjoint implies $U$ is $T$-invariant if and only if $U^\bot$ is $T$-invariant

theorem ker_ortho_adjoint_range {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (T : V →ₗ[𝕜] W) : LinearMap.ker T = (LinearMap.range (LinearMap.adjoint T))ᗮ

$\textnormal{ker}(T) = \textnormal{range}(T^*)^\bot$

theorem LinearMap.IsProj.isCompl_range_ker {V : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup V] [Module R V] (U : Submodule R V) (T : V →ₗ[R] V) (h : LinearMap.IsProj U T) : IsCompl (LinearMap.ker T) (LinearMap.range T)

given any idempotent operator $T \in L(V)$, then is_compl T.ker T.range, in other words, there exists unique $v \in \textnormal{ker}(T)$ and $w \in \textnormal{range}(T)$ such that $x = v + w$

theorem LinearMap.is_idempotent_isSelfAdjoint_iff_ker_ortho_range {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (T : V →ₗ[ℂ] V) (h : IsIdempotentElem T) : IsSelfAdjoint T ↔ (LinearMap.ker T)ᗮ = LinearMap.range T

idempotent $T$ is self-adjoint if and only if $\textnormal{ker}(T)^\bot=\textnormal{range}(T)$

theorem LinearMap.isStarNormal_iff_adjoint {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →ₗ[𝕜] V) : IsStarNormal T ↔ Commute T (LinearMap.adjoint T)

linear map is_star_normal if and only if it commutes with its adjoint

theorem ContinuousLinearMap.isStarNormal_iff_adjoint {V : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (T : V →L[𝕜] V) : IsStarNormal T ↔ Commute T (ContinuousLinearMap.adjoint T)

theorem isSymmetric_hMul_adjoint_self {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →ₗ[𝕜] V) : (T * LinearMap.adjoint T).IsSymmetric

theorem IsSymmetric.neg {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (T : V →ₗ[𝕜] V) (hT : T.IsSymmetric) : (-T).IsSymmetric

theorem IsSymmetric.sub {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {T : V →ₗ[𝕜] V} {S : V →ₗ[𝕜] V} (hT : T.IsSymmetric) (hS : S.IsSymmetric) : (T - S).IsSymmetric

theorem LinearMap.IsStarNormal.norm_eq_adjoint {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →ₗ[𝕜] V) : IsStarNormal T ↔ ∀ (v : V), ‖T v‖ = ‖(LinearMap.adjoint T) v‖

$T$ is normal if and only if $\forall v, \|T v\| = \|T^* v\|$

theorem ContinuousLinearMap.IsStarNormal.norm_eq_adjoint {V : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (T : V →L[𝕜] V) : IsStarNormal T ↔ ∀ (v : V), ‖T v‖ = ‖(ContinuousLinearMap.adjoint T) v‖

theorem LinearMap.IsStarNormal.ker_eq_ker_adjoint {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (T : V →ₗ[ℂ] V) (h : IsStarNormal T) : LinearMap.ker T = LinearMap.ker (LinearMap.adjoint T)

if $T$ is normal, then $\textnormal{ker}(T) = \textnormal{ker}(T^*)$

theorem LinearMap.IsStarNormal.range_eq_range_adjoint {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (T : V →ₗ[ℂ] V) (h : IsStarNormal T) : LinearMap.range T = LinearMap.range (LinearMap.adjoint T)

if $T$ is normal, then $\textnormal{range}(T)=\textnormal{range}(T^*)$

theorem ContinuousLinearMap.IsStarNormal.ker_eq_ker_adjoint {V : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {T : V →L[𝕜] V} (h : IsStarNormal T) : LinearMap.ker T = LinearMap.ker (ContinuousLinearMap.adjoint T)

theorem ContinuousLinearMap.ker_eq_ortho_adjoint_range {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace V] [CompleteSpace W] (T : V →L[𝕜] W) : LinearMap.ker T = (LinearMap.range (ContinuousLinearMap.adjoint T))ᗮ

theorem ContinuousLinearMap.ker_adjoint_eq_ortho_range {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace V] [CompleteSpace W] (T : V →L[𝕜] W) : LinearMap.ker (ContinuousLinearMap.adjoint T) = (LinearMap.range T)ᗮ

theorem ContinuousLinearMap.ker_adjoint_ortho_eq_range {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace V] [CompleteSpace W] (T : V →L[𝕜] W) [HasOrthogonalProjection (LinearMap.range T)] : (LinearMap.ker (ContinuousLinearMap.adjoint T))ᗮ = LinearMap.range T

theorem ContinuousLinearMap.IsStarNormal.isCompl_ker_range {V : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (T : V →L[𝕜] V) [CompleteSpace V] [HasOrthogonalProjection (LinearMap.range T)] (h : IsStarNormal T) : IsCompl (LinearMap.ker T) (LinearMap.range T)

theorem ContinuousLinearMap.IsIdempotentElem.toLinearMap {E : Type u_1} {R : Type u_2} [Ring R] [AddCommMonoid E] [Module R E] [TopologicalSpace E] (T : E →L[R] E) : IsIdempotentElem T ↔ IsIdempotentElem ↑T

theorem ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_ker_isOrtho_to_range {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (T : V →L[ℂ] V) (h : IsIdempotentElem T) : IsSelfAdjoint T ↔ LinearMap.ker T = (LinearMap.range T)ᗮ

theorem LinearMap.IsStarNormal.eigenvec_in_eigenspace_iff_eigenvec_in_adjoint_conj_eigenspace {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (T : V →ₗ[ℂ] V) (h : IsStarNormal T) (μ : ℂ) (x : V) : x ∈ Module.End.eigenspace T μ ↔ x ∈ Module.End.eigenspace (LinearMap.adjoint T) ((starRingEnd ℂ) μ)

if $T$ is normal, then $\forall x \in V, x \in \textnormal{eigenspace}(T ,\mu) \iff x \in \textnormal{eigenspace}(T^* ,\bar{\mu})$

theorem ContinuousLinearMap.ker_to_linearMap_ker {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (T : V →L[𝕜] W) : LinearMap.ker T = LinearMap.ker ↑T

theorem ContinuousLinearMap.adjoint_injective_iff_surjective {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace W] [CompleteSpace V] (T : V →L[𝕜] W) [HasOrthogonalProjection (LinearMap.range T)] : Function.Injective ⇑(ContinuousLinearMap.adjoint T) ↔ Function.Surjective ⇑T

$T$ is injective if and only if $T^*$ is surjective

theorem LinearMap.injective_iff_adjoint_surjective {V : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {W : Type u_1} [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] [FiniteDimensional 𝕜 V] (T : V →ₗ[𝕜] W) : Function.Injective ⇑T ↔ Function.Surjective ⇑(LinearMap.adjoint T)

$T$ is injective if and only if $T^*$ is surjective