monlib / linear_algebra.my_ips.ips

source

theorem submodule.invariant_under_iff_ortho_adjoint_invariant {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] (U : submodule 𝕜 V) (T : V →ₗ[𝕜] V) :

U.invariant_under T ↔ Uᗮ.invariant_under (⇑linear_map.adjoint T)

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

source

theorem submodule.invariant_under_iff_ortho_adjoint_invariant' {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] (U : submodule 𝕜 V) [complete_space V] [complete_space ↥U] (T : V →L[𝕜] V) :

U.invariant_under ↑T ↔ Uᗮ.invariant_under ↑(⇑continuous_linear_map.adjoint T)

source

theorem is_self_adjoint.submodule_invariant_iff_ortho_submodule_invariant {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] (U : submodule 𝕜 V) (T : V →ₗ[𝕜] V) (h : is_self_adjoint T) :

U.invariant_under T ↔ Uᗮ.invariant_under T

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

source

theorem ker_is_ortho_adjoint_range {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] {W : Type u_3} [finite_dimensional 𝕜 V] [normed_add_comm_group W] [inner_product_space 𝕜 W] [finite_dimensional 𝕜 W] (T : V →ₗ[𝕜] W) :

linear_map.ker T = (linear_map.range (⇑linear_map.adjoint T))ᗮ

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

source

theorem linear_map.is_proj.is_compl_range_ker {V : Type u_1} {R : Type u_2} [ring R] [add_comm_group V] [module R V] (U : submodule R V) (T : V →ₗ[R] V) (h : linear_map.is_proj U T) :

is_compl (linear_map.ker T) (linear_map.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$

source

theorem linear_map.is_idempotent_is_self_adjoint_iff_ker_is_ortho_to_range {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : V →ₗ[ℂ ] V) (h : is_idempotent_elem T) :

is_self_adjoint T ↔ (linear_map.ker T)ᗮ = linear_map.range T

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

source

theorem linear_map.is_star_normal_iff_adjoint {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] (T : V →ₗ[𝕜] V) :

is_star_normal T ↔ commute T (⇑linear_map.adjoint T)

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

source

theorem continuous_linear_map.is_star_normal_iff_adjoint {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [complete_space V] (T : V →L[𝕜] V) :

is_star_normal T ↔ commute T (⇑continuous_linear_map.adjoint T)

source

theorem is_symmetric_mul_adjoint_self {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] (T : V →ₗ[𝕜] V) :

(T * ⇑linear_map.adjoint T).is_symmetric

source

theorem is_symmetric.neg {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] (T : V →ₗ[𝕜] V) (hT : T.is_symmetric) :

(-T).is_symmetric

source

theorem is_symmetric.sub {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] {T S : V →ₗ[𝕜] V} (hT : T.is_symmetric) (hS : S.is_symmetric) :

(T - S).is_symmetric

source

theorem linear_map.is_star_normal.norm_eq_adjoint {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] (T : V →ₗ[𝕜] V) :

is_star_normal T ↔ ∀ (v : V), ‖⇑T v‖ = ‖⇑(⇑linear_map.adjoint T) v‖

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

source

theorem continuous_linear_map.is_star_normal.norm_eq_adjoint {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [complete_space V] (T : V →L[𝕜] V) :

is_star_normal T ↔ ∀ (v : V), ‖⇑T v‖ = ‖⇑(⇑continuous_linear_map.adjoint T) v‖

source

theorem linear_map.is_star_normal.ker_eq_ker_adjoint {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : V →ₗ[ℂ ] V) (h : is_star_normal T) :

linear_map.ker T = linear_map.ker (⇑linear_map.adjoint T)

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

source

theorem linear_map.is_star_normal.range_eq_range_adjoint {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : V →ₗ[ℂ ] V) (h : is_star_normal T) :

linear_map.range T = linear_map.range (⇑linear_map.adjoint T)

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

source

theorem continuous_linear_map.is_star_normal.ker_eq_ker_adjoint {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [complete_space V] (T : V →L[𝕜] V) (h : is_star_normal T) :

linear_map.ker T.to_linear_map = linear_map.ker (⇑continuous_linear_map.adjoint T).to_linear_map

source

theorem continuous_linear_map.ker_is_eq_ortho_adjoint_range {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] {W : Type u_3} [normed_add_comm_group W] [inner_product_space 𝕜 W] [complete_space V] [complete_space W] (T : V →L[𝕜] W) :

linear_map.ker T.to_linear_map = (linear_map.range (⇑continuous_linear_map.adjoint T).to_linear_map)ᗮ

source

theorem continuous_linear_map.is_star_normal.is_compl_ker_range {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] [complete_space V] (T : V →L[𝕜] V) [finite_dimensional 𝕜 V] (h : is_star_normal T) :

is_compl (linear_map.ker T.to_linear_map) (linear_map.range T.to_linear_map)

source

theorem continuous_linear_map.is_idempotent_elem.to_linear_map {E : Type u_1} {R : Type u_2} [ring R] [add_comm_monoid E] [module R E] [topological_space E] (T : E →L[R] E) :

is_idempotent_elem T ↔ is_idempotent_elem T.to_linear_map

source

theorem continuous_linear_map.is_idempotent.is_self_adjoint_iff_ker_is_ortho_to_range {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℂ V] [complete_space V] (T : V →L[ℂ ] V) (h : is_idempotent_elem T) :

is_self_adjoint T ↔ linear_map.ker T.to_linear_map = (linear_map.range T.to_linear_map)ᗮ

source

theorem linear_map.is_star_normal.eigenvec_in_eigenspace_iff_eigenvec_in_adjoint_conj_eigenspace {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : V →ₗ[ℂ ] V) (h : is_star_normal T) (μ : ℂ) (x : V) :

x ∈ module.End.eigenspace T μ ↔ x ∈ module.End.eigenspace (⇑linear_map.adjoint T) (⇑(star_ring_end ℂ) μ)

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

source

theorem linear_map.injective_iff_adjoint_surjective {V : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group V] [inner_product_space 𝕜 V] {W : Type u_3} [normed_add_comm_group W] [inner_product_space 𝕜 W] [finite_dimensional 𝕜 W] [finite_dimensional 𝕜 V] (T : V →ₗ[𝕜] W) :

function.injective ⇑T ↔ function.surjective ⇑(⇑linear_map.adjoint T)

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

mathlib3 documentation

Finite-dimensional inner product spaces #

Notation #