Positive linear maps #
This file generalises the notion of positivity to linear maps. We follow the same definition as continuous_linear_map.is_positive 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.is_positive.conj_adjoint: ifT : E →ₗ[𝕜] EandEis a finite-dimensional space, then for anyS : E →ₗ[𝕜] F, we haveS.comp (T.comp S.adjoint)is also positive.
def
linear_map.is_positive
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(T : E →ₗ[𝕜] E) :
Prop
T is (semi-definite) positive if T is symmetric
and ∀ x : V, 0 ≤ re ⟪x, T x⟫
Equations
- T.is_positive = (T.is_symmetric ∧ ∀ (x : E), 0 ≤ ⇑is_R_or_C.re (has_inner.inner x (⇑T x)))
theorem
linear_map.is_positive_zero
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E] :
theorem
linear_map.is_positive_one
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E] :
theorem
linear_map.is_positive.add
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{S T : E →ₗ[𝕜] E}
(hS : S.is_positive)
(hT : T.is_positive) :
(S + T).is_positive
theorem
linear_map.is_positive.inner_nonneg_left
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{T : E →ₗ[𝕜] E}
(hT : T.is_positive)
(x : E) :
0 ≤ ⇑is_R_or_C.re (has_inner.inner (⇑T x) x)
theorem
linear_map.is_positive.inner_nonneg_right
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{T : E →ₗ[𝕜] E}
(hT : T.is_positive)
(x : E) :
0 ≤ ⇑is_R_or_C.re (has_inner.inner x (⇑T x))
theorem
linear_map.linear_proj_is_positive_iff
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{U V : submodule 𝕜 E}
(hUV : is_compl U V) :
(U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_positive ↔ U ⟂ V
a linear projection onto U along its complement V is positive if
and only if U and V are pairwise orthogonal
theorem
linear_map.is_positive.nonneg_spectrum
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(h : T.is_positive) :
the spectrum of a positive linear map is non-negative
theorem
linear_map.sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_symmetric)
(hT1 : (spectrum 𝕜 T).is_nonneg)
(v : E) :
⇑T v = finset.univ.sum (λ (i : fin n), (real.sqrt (hT.eigenvalues hn i) • ↑(real.sqrt (hT.eigenvalues hn i))) • has_inner.inner (⇑(hT.eigenvector_basis hn) i) v • ⇑(hT.eigenvector_basis hn) 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 (is_symmetric.eigenvector_basis)
noncomputable
def
linear_map.re_pow
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_symmetric)
(r : ℝ) :
given a symmetric linear map T and a real number r,
we can define a linear map S such that S = T ^ r
Equations
- T.re_pow hn hT r = {to_fun := λ (v : E), finset.univ.sum (λ (i : fin n), ↑(hT.eigenvalues hn i ^ r) • has_inner.inner (⇑(hT.eigenvector_basis hn) i) v • ⇑(hT.eigenvector_basis hn) i), map_add' := _, map_smul' := _}
noncomputable
def
linear_map.cpow
{E : Type u_2}
[normed_add_comm_group E]
{n : ℕ}
[inner_product_space ℂ E]
[finite_dimensional ℂ E]
[decidable_eq ℂ]
(hn : finite_dimensional.finrank ℂ E = n)
(T : E →ₗ[ℂ] E)
(hT : T.is_positive)
(c : ℂ) :
Equations
- linear_map.cpow hn T hT c = {to_fun := λ (v : E), finset.univ.sum (λ (i : fin n), ↑(_.eigenvalues hn i) ^ c • has_inner.inner (⇑(_.eigenvector_basis hn) i) v • ⇑(_.eigenvector_basis hn) i), map_add' := _, map_smul' := _}
theorem
linear_map.cpow_apply
{E : Type u_2}
[normed_add_comm_group E]
{n : ℕ}
[inner_product_space ℂ E]
[finite_dimensional ℂ E]
[decidable_eq ℂ]
(hn : finite_dimensional.finrank ℂ E = n)
(T : E →ₗ[ℂ] E)
(hT : T.is_positive)
(c : ℂ)
(v : E) :
⇑(linear_map.cpow hn T hT c) v = finset.univ.sum (λ (i : fin n), ↑(_.eigenvalues hn i) ^ c • has_inner.inner (⇑(_.eigenvector_basis hn) i) v • ⇑(_.eigenvector_basis hn) i)
theorem
linear_map.re_pow_apply
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_symmetric)
(r : ℝ)
(v : E) :
⇑(T.re_pow hn hT r) v = finset.univ.sum (λ (i : fin n), ↑(hT.eigenvalues hn i ^ r) • has_inner.inner (⇑(hT.eigenvector_basis hn) i) v • ⇑(hT.eigenvector_basis hn) i)
noncomputable
def
linear_map.sqrt
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 E = n)
(h : T.is_symmetric) :
the square root of a symmetric linear map can then directly be defined with re_pow
theorem
linear_map.sqrt_apply
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq 𝕜]
(hT : T.is_symmetric)
(x : E) :
⇑(T.sqrt hn hT) x = finset.univ.sum (λ (i : fin n), ↑(real.sqrt (hT.eigenvalues hn i)) • has_inner.inner (⇑(hT.eigenvector_basis hn) i) x • ⇑(hT.eigenvector_basis hn) 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 (is_symmetric.eigenvector_basis)
theorem
linear_map.sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_symmetric)
(hT1 : (spectrum 𝕜 T).is_nonneg) :
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
linear_map.is_symmetric.sqrt_is_positive
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_symmetric) :
(T.sqrt hn hT).is_positive
given a symmetric linear map T, we have that its root is positive
theorem
linear_map.is_positive_iff_is_symmetric_and_nonneg_spectrum
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hn : finite_dimensional.finrank 𝕜 E = n) :
T.is_positive ↔ T.is_symmetric ∧ (spectrum 𝕜 T).is_nonneg
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
linear_map.is_positive_iff_exists_adjoint_mul_self
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hn : finite_dimensional.finrank 𝕜 E = n) :
T.is_positive ↔ ∃ (S : E →ₗ[𝕜] E), T = ⇑linear_map.adjoint S * S
T is positive if and only if there exists a
linear map S such that T = S.adjoint * S
theorem
linear_map.complex_is_positive
{V : Type u_1}
[normed_add_comm_group V]
[inner_product_space ℂ V]
(T : V →ₗ[ℂ] V) :
T.is_positive ↔ ∀ (v : V), ↑(⇑is_R_or_C.re (has_inner.inner v (⇑T v))) = has_inner.inner v (⇑T v) ∧ 0 ≤ ⇑is_R_or_C.re (has_inner.inner v (⇑T v))
for spaces V over ℂ, it suffices to define positivity with
0 ≤ ⟪v, T v⟫_ℂ for all v ∈ V
theorem
linear_map.is_positive.conj_adjoint
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[normed_add_comm_group F]
[inner_product_space 𝕜 E]
[inner_product_space 𝕜 F]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
(T : E →ₗ[𝕜] E)
(S : E →ₗ[𝕜] F)
(h : T.is_positive) :
(S.comp (T.comp (⇑linear_map.adjoint S))).is_positive
theorem
linear_map.is_positive.adjoint_conj
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[normed_add_comm_group F]
[inner_product_space 𝕜 E]
[inner_product_space 𝕜 F]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
(T : E →ₗ[𝕜] E)
(S : F →ₗ[𝕜] E)
(h : T.is_positive) :
((⇑linear_map.adjoint S).comp (T.comp S)).is_positive
theorem
linear_map.sqrt_adjoint_self_is_positive
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq 𝕜]
(T : E →ₗ[𝕜] E) :
(((⇑linear_map.adjoint T).comp T).sqrt hn _).is_positive
we have (T.adjoint.comp T).sqrt is positive, given any linear map T
theorem
linear_map.norm_of_sqrt_adjoint_mul_self_eq
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq 𝕜]
(T : E →ₗ[𝕜] E)
(x : E) :
given any linear map T and x ∈ E we have
‖(T.adjoint.comp T).sqrt x‖ = ‖T x‖
theorem
linear_map.invertible_iff_inner_map_self_pos
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_positive) :
function.bijective ⇑T ↔ ∀ (v : E), v ≠ 0 → 0 < ⇑is_R_or_C.re (has_inner.inner (⇑T v) v)
theorem
linear_map.ext_inner_left_iff
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(x y : E) :
x = y ↔ ∀ (v : E), has_inner.inner x v = has_inner.inner y v
theorem
linear_map.invertible_pos
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
[invertible T]
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_positive) :
(⅟ T).is_positive
theorem
linear_map.is_symmetric.re_pow_eq_rank_one
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
[decidable_eq 𝕜]
{n : ℕ}
(hn : finite_dimensional.finrank 𝕜 E = n)
{T : E →ₗ[𝕜] E}
(hT : T.is_symmetric)
(r : ℝ) :
T.re_pow hn hT r = finset.univ.sum (λ (i : fin n), ↑(hT.eigenvalues hn i ^ r) • ↑(rank_one (⇑(hT.eigenvector_basis hn) i) (⇑(hT.eigenvector_basis hn) i)))
theorem
linear_map.is_symmetric.invertible
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hT : T.is_symmetric)
[invertible T] :
(⅟ T).is_symmetric
theorem
linear_map.is_positive_and_invertible_pos_eigenvalues
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hn : finite_dimensional.finrank 𝕜 E = n)
(hT : T.is_positive)
[invertible T]
[decidable_eq 𝕜]
(i : fin n) :
0 < _.eigenvalues hn i
noncomputable
def
linear_map.is_positive.re_pow_is_invertible
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[finite_dimensional 𝕜 E]
(T : E →ₗ[𝕜] E)
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq 𝕜]
(hT : T.is_positive)
[invertible T]
(r : ℝ) :
invertible (T.re_pow hn _ r)
Equations
- linear_map.is_positive.re_pow_is_invertible T hn hT r = {inv_of := T.re_pow hn _ (-r), inv_of_mul_self := _, mul_inv_of_self := _}
theorem
linear_map.is_positive.sum
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
{T : fin n → (E →ₗ[𝕜] E)}
(hT : ∀ (i : fin n), (T i).is_positive) :
(finset.univ.sum (λ (i : fin n), T i)).is_positive
theorem
linear_map.is_positive.smul_nonneg
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{T : E →ₗ[𝕜] E}
(hT : T.is_positive)
{r : ℝ}
(hr : 0 ≤ r) :
(↑r • T).is_positive
theorem
continuous_linear_map.is_positive.to_linear_map
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
(T : E →L[𝕜] E) :
theorem
rank_one.is_positive
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
(x : E) :
(rank_one x x).is_positive
theorem
linear_map.is_positive.nonneg_eigenvalue
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
{T : E →ₗ[𝕜] E}
(hT : T.is_positive)
{α : ℝ}
(hα : module.End.has_eigenvalue T ↑α) :
0 ≤ α
theorem
linear_map.is_positive_iff_eq_sum_rank_one
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{n : ℕ}
[decidable_eq 𝕜]
[finite_dimensional 𝕜 E]
(hn : finite_dimensional.finrank 𝕜 E = n)
(T : E →ₗ[𝕜] E) :
theorem
linear_map.is_symmetric.re_pow_is_positive_of_is_positive
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
[decidable_eq 𝕜]
{n : ℕ}
(hn : finite_dimensional.finrank 𝕜 E = n)
{T : E →ₗ[𝕜] E}
(hT : T.is_positive)
(r : ℝ) :
(T.re_pow hn _ r).is_positive