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.IsPositive'Zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : IsPositive' 0

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

theorem LinearMap.IsPositive'.add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S 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 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 ContinuousLinearMap.IsPositive.toLinearMap' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) : T.IsPositive ↔ (↑T).IsPositive'

theorem LinearMap.isPositive'_iff_isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : T.IsPositive' ↔ T.IsPositive

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

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 = 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 ∘ₗ 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') : (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) : ((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) : ‖((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 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.rePowIsPositive'OfIsPositive' {𝕜 : 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'