Positive linear maps

This file generalises the notion of positivity to linear maps. We follow the same definition as continuous_linear_map.isPositive but change the self-adjoinnt property to is_symmertric, i.e., a linear map is positive if it is symmetric and ∀ x, 0 ≤ re ⟪T x, x⟫

Main statements

for linear maps:

• linear_map.isPositive.conj_adjoint : if T : E →ₗ[𝕜] E and E is a finite-dimensional space, then for any S : E →ₗ[𝕜] F, we have S.comp (T.comp S.adjoint) is also positive.

def LinearMap.IsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) : Prop

T is (semi-definite) positive if T is symmetric and ∀ x : V, 0 ≤ re ⟪x, T x⟫

Equations

• T.IsPositive = (T.IsSymmetric ∧ ∀ (x : E), 0 ≤ inner x (T x))

theorem LinearMap.isPositiveZero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : LinearMap.IsPositive 0

theorem LinearMap.isPositiveOne {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : LinearMap.IsPositive 1

theorem LinearMap.IsPositive.add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : E →ₗ[𝕜] E} {T : E →ₗ[𝕜] E} (hS : S.IsPositive) (hT : T.IsPositive) : (S + T).IsPositive

theorem LinearMap.IsPositive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) : 0 ≤ inner (T x) x

theorem LinearMap.IsPositive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) : 0 ≤ inner x (T x)

theorem LinearMap.linear_proj_isPositive_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {V : Submodule 𝕜 E} (hUV : IsCompl U V) : (U.subtype ∘ₗ U.linearProjOfIsCompl V hUV).IsPositive ↔ U ⟂ V

a linear projection onto U along its complement V is positive if and only if U and V are pairwise orthogonal

theorem LinearMap.IsPositive.nonneg_spectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (h : T.IsPositive) : spectrum 𝕜 T ⊆ {x : 𝕜 | 0 ≤ x}

the spectrum of a positive linear map is non-negative

theorem LinearMap.sq_mul_sq_eq_self_of_isSymmetric_and_nonneg_spectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) (hT1 : spectrum 𝕜 T ⊆ {x : 𝕜 | 0 ≤ x}) (v : E) : T v = ∑ i : Fin (Module.finrank 𝕜 E), (√(hT.eigenvalues ⋯ i) • ↑√(hT.eigenvalues ⋯ i)) • inner ((hT.eigenvectorBasis ⋯) i) v • (hT.eigenvectorBasis ⋯) i

given a symmetric linear map with a non-negative spectrum, we can write T x = ∑ i, √α i • √α i • ⟪e i, x⟫ for any x ∈ E, where α i are the eigenvalues of T and e i are the respective eigenvectors that form an eigenbasis (isSymmetric.eigenvector_basis)

noncomputable def LinearMap.rePow {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) (r : ℝ) : E →ₗ[𝕜] E

given a symmetric linear map T and a real number r, we can define a linear map S such that S = T ^ r

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LinearMap.cpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (T : E →ₗ[ℂ] E) (hT : T.IsPositive) (c : ℂ) : E →ₗ[ℂ] E

Equations

• One or more equations did not get rendered due to their size.

theorem LinearMap.cpow_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (T : E →ₗ[ℂ] E) (hT : T.IsPositive) (c : ℂ) (v : E) : (T.cpow hT c) v = ∑ i : Fin (Module.finrank ℂ E), ↑(⋯.eigenvalues ⋯ i) ^ c • inner ((⋯.eigenvectorBasis ⋯) i) v • (⋯.eigenvectorBasis ⋯) i

theorem LinearMap.rePow_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) (r : ℝ) (v : E) : (T.rePow hT r) v = ∑ i : Fin (Module.finrank 𝕜 E), ↑(hT.eigenvalues ⋯ i ^ r) • inner ((hT.eigenvectorBasis ⋯) i) v • (hT.eigenvectorBasis ⋯) i

noncomputable def LinearMap.sqrt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (h : T.IsSymmetric) : E →ₗ[𝕜] E

the square root of a symmetric linear map can then directly be defined with re_pow

Equations

• T.sqrt h = T.rePow h (1 / 2)

theorem LinearMap.sqrt_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) (x : E) : (T.sqrt hT) x = ∑ i : Fin (Module.finrank 𝕜 E), ↑√(hT.eigenvalues ⋯ i) • inner ((hT.eigenvectorBasis ⋯) i) x • (hT.eigenvectorBasis ⋯) i

the square root of a symmetric linear map T is written as T x = ∑ i, √ (α i) • ⟪e i, x⟫ • e i for any x ∈ E, where α i are the eigenvalues of T and e i are the respective eigenvectors that form an eigenbasis (isSymmetric.eigenvector_basis)

theorem LinearMap.sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) (hT1 : spectrum 𝕜 T ⊆ {x : 𝕜 | 0 ≤ x}) : T.sqrt hT ^ 2 = T

given a symmetric linear map T with a non-negative spectrum, the square root of T composed with itself equals itself, i.e., T.sqrt ^ 2 = T

theorem LinearMap.IsSymmetric.sqrtIsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) : (T.sqrt hT).IsPositive

given a symmetric linear map T, we have that its root is positive

theorem LinearMap.isPositive_iff_isSymmetric_and_nonneg_spectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : T.IsPositive ↔ T.IsSymmetric ∧ spectrum 𝕜 T ⊆ {x : 𝕜 | 0 ≤ x}

T is positive if and only if T is symmetric (which is automatic from the definition of positivity) and has a non-negative spectrum

theorem LinearMap.isPositive_iff_exists_adjoint_hMul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : T.IsPositive ↔ ∃ (S : E →ₗ[𝕜] E), T = LinearMap.adjoint S * S

T is positive if and only if there exists a linear map S such that T = S.adjoint * S

theorem LinearMap.complex_isPositive {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) : T.IsPositive ↔ ∀ (v : V), 0 ≤ inner v (T v)

for spaces V over ℂ, it suffices to define positivity with 0 ≤ ⟪v, T v⟫_ℂ for all v ∈ V

theorem LinearMap.IsPositive.conjAdjoint {𝕜 : Type u_1} {E : Type u_3} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] E) (S : E →ₗ[𝕜] F) (h : T.IsPositive) : (S ∘ₗ T ∘ₗ LinearMap.adjoint S).IsPositive

theorem LinearMap.IsPositive.adjointConj {𝕜 : Type u_1} {E : Type u_3} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] E) (S : F →ₗ[𝕜] E) (h : T.IsPositive) : (LinearMap.adjoint S ∘ₗ T ∘ₗ S).IsPositive

theorem LinearMap.sqrtAdjointSelfIsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : ((LinearMap.adjoint T ∘ₗ T).sqrt ⋯).IsPositive

we have (T.adjoint.comp T).sqrt is positive, given any linear map T

theorem LinearMap.norm_of_sqrt_adjoint_mul_self_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) : ‖((LinearMap.adjoint T ∘ₗ T).sqrt ⋯) x‖ = ‖T x‖

given any linear map T and x ∈ E we have ‖(T.adjoint.comp T).sqrt x‖ = ‖T x‖

theorem LinearMap.invertible_iff_inner_map_self_pos {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsPositive) : Function.Bijective ⇑T ↔ ∀ (v : E), v ≠ 0 → 0 < inner (T v) v

theorem LinearMap.invertiblePos {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) [hTi : Invertible T] (hT : T.IsPositive) : (⅟T).IsPositive

theorem LinearMap.IsSymmetric.rePow_eq_rankOne {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (r : ℝ) : T.rePow hT r = ↑(∑ i : Fin (Module.finrank 𝕜 E), ↑(hT.eigenvalues ⋯ i ^ r) • ((rankOne 𝕜) ((hT.eigenvectorBasis ⋯) i)) ((hT.eigenvectorBasis ⋯) i))

theorem LinearMap.IsSymmetric.invertible {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsSymmetric) [Invertible T] : (⅟T).IsSymmetric

theorem LinearMap.isPositive_and_invertible_pos_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsPositive) [Invertible T] (i : Fin (Module.finrank 𝕜 E)) : 0 < ⋯.eigenvalues ⋯ i

noncomputable def LinearMap.IsPositive.rePowIsInvertible {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hT : T.IsPositive) [Invertible T] (r : ℝ) : Invertible (T.rePow ⋯ r)

Equations

• LinearMap.IsPositive.rePowIsInvertible T hT r = { invOf := T.rePow ⋯ (-r), invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem LinearMap.IsPositive.sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} {T : Fin n → E →ₗ[𝕜] E} (hT : ∀ (i : Fin n), (T i).IsPositive) : (∑ i : Fin n, T i).IsPositive

theorem LinearMap.IsPositive.smulNonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) {r : ℝ} (hr : 0 ≤ r) : (↑r • T).IsPositive

theorem LinearMap.IsPositive.smulNNReal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (r : NNReal) : (↑↑r • T).IsPositive

theorem ContinuousLinearMap.IsPositive.toLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : (↑T).IsPositive ↔ T.IsPositive

theorem rankOne_self_isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {x : E} : (((rankOne 𝕜) x) x).IsPositive

theorem LinearMap.IsPositive.nonneg_eigenvalue {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) {α : ℝ} (hα : Module.End.HasEigenvalue T ↑α) : 0 ≤ α

theorem LinearMap.isPositive_iff_eq_sum_rankOne {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : T.IsPositive ↔ ∃ (m : ℕ) (u : Fin m → E), T = ∑ i : Fin m, ↑(((rankOne 𝕜) (u i)) (u i))

theorem LinearMap.IsSymmetric.rePowIsPositiveOfIsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (r : ℝ) : (T.rePow ⋯ r).IsPositive