From 4831680ae014e6952e1c5bffcb4614bcf3c00488 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 19 Jan 2023 16:35:00 +0000 Subject: [PATCH 1/9] chore(inner_product_space/positive): some lemmas --- .../inner_product_space/positive.lean | 199 +++++++++++++++++- 1 file changed, 198 insertions(+), 1 deletion(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index 46fd7ddd5b7ad..5bb1ac70d9c2b 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Anatole Dedecker -/ import analysis.inner_product_space.adjoint +import analysis.inner_product_space.spectrum /-! # Positive operators @@ -33,10 +34,11 @@ of requiring self adjointness in the definition. Positive operator -/ +namespace continuous_linear_map + open inner_product_space is_R_or_C continuous_linear_map open_locale inner_product complex_conjugate -namespace continuous_linear_map variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] [complete_space E] [complete_space F] @@ -124,3 +126,198 @@ end end complex end continuous_linear_map + +namespace linear_map + +open linear_map + +variables {V : Type*} [inner_product_space โ„‚ V] + +local notation `e` := is_symmetric.eigenvector_basis +open_locale big_operators + +/-- `T` is (semi-definite) positive if `โˆ€ x : V, โŸชx, T xโŸซ_โ„‚ โ‰ฅ 0` -/ +def is_positive (T : V โ†’โ‚—[โ„‚] V) : + Prop := โˆ€ x : V, 0 โ‰ค โŸชx, T xโŸซ_โ„‚.re โˆง (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ + +lemma is_self_adjoint_iff_real_inner [finite_dimensional โ„‚ V] (T : V โ†’โ‚—[โ„‚] V) : + is_self_adjoint T โ†” โˆ€ x, (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ := +begin + simp_rw [โ† is_symmetric_iff_is_self_adjoint, is_symmetric_iff_inner_map_self_real, + inner_conj_sym, โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re, + inner_conj_sym], + exact โŸจฮป h x, (h x).symm, ฮป h x, (h x).symmโŸฉ, +end + +/-- if `T.is_positive`, then `T.is_self_adjoint` and all its eigenvalues are non-negative -/ +lemma is_positive.self_adjoint_and_nonneg_spectrum [finite_dimensional โ„‚ V] + (T : V โ†’โ‚—[โ„‚] V) (h : T.is_positive) : + is_self_adjoint T โˆง โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = ฮผ.re โˆง 0 โ‰ค ฮผ.re := +begin + have frs : is_self_adjoint T, + { rw linear_map.is_self_adjoint_iff', + symmetry, + rw [โ† sub_eq_zero, โ† inner_map_self_eq_zero], + intro x, + cases h x, + have := complex.re_add_im (inner x (T x)), + rw [โ† right, complex.of_real_re, complex.of_real_im] at this, + rw [linear_map.sub_apply, inner_sub_left, โ† inner_conj_sym, linear_map.adjoint_inner_left, + โ† right, is_R_or_C.conj_of_real, sub_self], }, + refine โŸจfrs,_โŸฉ, + intros ฮผ hฮผ, + rw โ† module.End.has_eigenvalue_iff_mem_spectrum at hฮผ, + have realeigen := (complex.eq_conj_iff_re.mp + (linear_map.is_symmetric.conj_eigenvalue_eq_self + ((linear_map.is_symmetric_iff_is_self_adjoint T).mpr frs) hฮผ)).symm, + refine โŸจrealeigen, _โŸฉ, + have hฮฑ : โˆƒ ฮฑ : โ„, ฮฑ = ฮผ.re := by use ฮผ.re, + cases hฮฑ with ฮฑ hฮฑ, + rw โ† hฮฑ, + rw [realeigen, โ† hฮฑ] at hฮผ, + exact eigenvalue_nonneg_of_nonneg hฮผ (ฮป x, ge_iff_le.mp (h x).1), +end + +variables [finite_dimensional โ„‚ V] {n : โ„•} (hn : finite_dimensional.finrank โ„‚ V = n) +variables (T : V โ†’โ‚—[โ„‚] V) + +lemma of_pos_eq_sqrt_sqrt (hT : T.is_symmetric) + (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) (v : V) : + T v = โˆ‘ (i : (fin n)), real.sqrt (hT.eigenvalues hn i) โ€ข real.sqrt (hT.eigenvalues hn i) + โ€ข โŸช(e hT hn) i, vโŸซ_โ„‚ โ€ข (e hT hn) i := +begin + have : โˆ€ i : fin n, 0 โ‰ค hT.eigenvalues hn i := ฮป i, + by { specialize hT1 (hT.eigenvalues hn i), + simp only [complex.of_real_re, eq_self_iff_true, true_and] at hT1, + apply hT1 (module.End.mem_spectrum_of_has_eigenvalue + (is_symmetric.has_eigenvalue_eigenvalues hT hn i)), }, + calc T v = โˆ‘ (i : (fin n)), โŸช(e hT hn) i, vโŸซ_โ„‚ โ€ข T ((e hT hn) i) : + by simp_rw [โ† orthonormal_basis.repr_apply_apply, โ† map_smul_of_tower, โ† linear_map.map_sum, + orthonormal_basis.sum_repr (is_symmetric.eigenvector_basis hT hn) v] + ... = โˆ‘ (i : (fin n)), + real.sqrt (hT.eigenvalues hn i) โ€ข real.sqrt (hT.eigenvalues hn i) โ€ข + โŸช(e hT hn) i, vโŸซ_โ„‚ โ€ข (e hT hn) i : + by simp_rw [is_symmetric.apply_eigenvector_basis, smul_smul, โ† real.sqrt_mul (this _), + real.sqrt_mul_self (this _), mul_comm, โ† smul_smul, complex.coe_smul], +end + +include hn +/-- Let `e = hT.eigenvector_basis hn` so that we have `T (e i) = ฮฑ i โ€ข e i` for each `i`. +Then when `T.is_symmetric` and all its eigenvalues are nonnegative, +we can define `T.sqrt` by `e i โ†ฆ โˆšฮฑ i โ€ข e i`. -/ +noncomputable def sqrt (hT : T.is_symmetric) : V โ†’โ‚—[โ„‚] V := +{ to_fun := ฮป v, โˆ‘ (i : (fin n)), + real.sqrt (hT.eigenvalues hn i) โ€ข โŸช(hT.eigenvector_basis hn) i, vโŸซ_โ„‚ + โ€ข (hT.eigenvector_basis hn) i, + map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], + map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, + ring_hom.id_apply, โ† complex.coe_smul, smul_smul, + โ† mul_assoc, mul_comm] } + +lemma sqrt_eq (hT : T.is_symmetric) (v : V) : (T.sqrt hn hT) v = โˆ‘ (i : (fin n)), + real.sqrt (hT.eigenvalues hn i) โ€ข โŸช(hT.eigenvector_basis hn) i, vโŸซ_โ„‚ + โ€ข (hT.eigenvector_basis hn) i := rfl + +/-- `T.sqrt ^ 2 = T` and `T.sqrt.is_positive` -/ +lemma sqrt_sq_eq_linear_map_and_is_positive (hT : T.is_symmetric) + (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) : + (T.sqrt hn hT)^2 = T โˆง (T.sqrt hn hT).is_positive := +begin + rw [pow_two, mul_eq_comp], + split, + { ext v, + simp only [comp_apply, linear_map.sqrt_eq, inner_sum, inner_smul_real_right], + simp only [โ† complex.coe_smul, smul_smul, inner_smul_right], + simp only [โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, + euclidean_space.single_apply, mul_boole, finset.sum_ite_eq, + finset.mem_univ, if_true, โ† smul_smul, complex.coe_smul], + symmetry, + simp only [orthonormal_basis.repr_apply_apply], + exact linear_map.of_pos_eq_sqrt_sqrt hn T hT hT1 v, }, + { intro, + split, + { simp_rw [linear_map.sqrt_eq, inner_sum, โ† complex.coe_smul, smul_smul, inner_smul_right, + complex.re_sum, mul_assoc, mul_comm, โ† complex.real_smul, โ† inner_conj_sym x, + โ† complex.norm_sq_eq_conj_mul_self, complex.smul_re, complex.of_real_re, + smul_eq_mul], + apply finset.sum_nonneg', + intros i, + specialize hT1 (hT.eigenvalues hn i), + simp only [complex.of_real_re, eq_self_iff_true, true_and] at hT1, + simp_rw [mul_nonneg_iff, real.sqrt_nonneg, complex.norm_sq_nonneg, and_self, true_or], }, + { suffices : โˆ€ x, (star_ring_end โ„‚) โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚ = โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚, + { rw [โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re], + exact this x, }, + intro x, + simp_rw [inner_conj_sym, linear_map.sqrt_eq, sum_inner, inner_sum, โ† complex.coe_smul, + smul_smul, inner_smul_left, inner_smul_right, map_mul, is_R_or_C.conj_of_real, + inner_conj_sym, mul_assoc, mul_comm โŸช_, xโŸซ_โ„‚], }, }, +end + +/-- `T.is_positive` if and only if `T.is_self_adjoint` and all its eigenvalues are nonnegative. -/ +theorem is_positive_iff_self_adjoint_and_nonneg_eigenvalues : + T.is_positive โ†” is_self_adjoint T โˆง (โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) := +begin + split, + { intro h, exact linear_map.is_positive.self_adjoint_and_nonneg_spectrum T h, }, + { intro h, + have hT : T.is_symmetric := (is_symmetric_iff_is_self_adjoint T).mpr h.1, + rw [โ† (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT h.2).1, pow_two], + have : (T.sqrt hn hT) * (T.sqrt hn hT) = (T.sqrt hn hT).adjoint * (T.sqrt hn hT) := + by rw is_self_adjoint_iff'.mp (linear_map.is_positive.self_adjoint_and_nonneg_spectrum _ + (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT h.2).2).1, + rw this, clear this, + intro, + simp_rw [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K], + norm_cast, refine โŸจsq_nonneg โ€–(linear_map.sqrt hn T hT) xโ€–, rflโŸฉ, }, +end + +/-- every positive linear map can be written as `S.adjoint * S` for some linear map `S` -/ +lemma is_positive_iff_exists_linear_map_mul_adjoint : + T.is_positive โ†” โˆƒ S : V โ†’โ‚—[โ„‚] V, T = S.adjoint * S := +begin + split, + { rw [linear_map.is_positive_iff_self_adjoint_and_nonneg_eigenvalues hn, + โ† is_symmetric_iff_is_self_adjoint], + rintro โŸจhT, hT1โŸฉ, + use T.sqrt hn hT, + rw [is_self_adjoint_iff'.mp (linear_map.is_positive.self_adjoint_and_nonneg_spectrum _ + (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT hT1).2).1, + โ† pow_two, (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT hT1).1], }, + { intros h x, + cases h with S hS, + simp_rw [hS, mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K], + norm_cast, + refine โŸจsq_nonneg _, rflโŸฉ, }, +end + +end linear_map + +section finite_dimensional + +variables (V : Type*) [inner_product_space โ„‚ V] [finite_dimensional โ„‚ V] (T : V โ†’L[โ„‚] V) + +open linear_map +lemma self_adjoint_clm_iff_self_adjoint_lm : + is_self_adjoint T โ†” is_self_adjoint T.to_linear_map := +begin + simp_rw [continuous_linear_map.to_linear_map_eq_coe, is_self_adjoint_iff', + continuous_linear_map.is_self_adjoint_iff', continuous_linear_map.ext_iff, + linear_map.ext_iff, continuous_linear_map.coe_coe, adjoint_eq_to_clm_adjoint], + split, + { intros h x, rw โ† h x, refl, }, + { intros h x, rw โ† h x, refl, }, +end + +lemma is_positive_clm_iff_is_positive_lm : + T.is_positive โ†” linear_map.is_positive T.to_linear_map := +begin + simp_rw [linear_map.is_positive, continuous_linear_map.is_positive, + self_adjoint_clm_iff_self_adjoint_lm, linear_map.is_self_adjoint_iff_real_inner, + continuous_linear_map.re_apply_inner_self_apply, inner_re_symm, + is_R_or_C.re_eq_complex_re, continuous_linear_map.to_linear_map_eq_coe, + continuous_linear_map.coe_coe, and.comm], + refine โŸจฮป h x, โŸจh.1 x, h.2 xโŸฉ, ฮป h, โŸจฮป x, (h x).1, ฮป x, (h x).2โŸฉโŸฉ, +end + +end finite_dimensional From 4c0719b7926e98e8d5e30f17fecb8583502e1dc0 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 24 Jan 2023 12:30:52 +0000 Subject: [PATCH 2/9] fix --- .../inner_product_space/positive.lean | 157 +++++++++--------- .../inner_product_space/symmetric.lean | 9 + 2 files changed, 88 insertions(+), 78 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index 5bb1ac70d9c2b..91b94805341e4 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -131,26 +131,20 @@ namespace linear_map open linear_map -variables {V : Type*} [inner_product_space โ„‚ V] - +variables {V ๐•œ : Type*} [is_R_or_C ๐•œ] [inner_product_space โ„‚ V] +open_locale inner_product complex_conjugate big_operators --complex_order +open is_R_or_C local notation `e` := is_symmetric.eigenvector_basis -open_locale big_operators +local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y /-- `T` is (semi-definite) positive if `โˆ€ x : V, โŸชx, T xโŸซ_โ„‚ โ‰ฅ 0` -/ -def is_positive (T : V โ†’โ‚—[โ„‚] V) : - Prop := โˆ€ x : V, 0 โ‰ค โŸชx, T xโŸซ_โ„‚.re โˆง (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ - -lemma is_self_adjoint_iff_real_inner [finite_dimensional โ„‚ V] (T : V โ†’โ‚—[โ„‚] V) : - is_self_adjoint T โ†” โˆ€ x, (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ := -begin - simp_rw [โ† is_symmetric_iff_is_self_adjoint, is_symmetric_iff_inner_map_self_real, - inner_conj_sym, โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re, - inner_conj_sym], - exact โŸจฮป h x, (h x).symm, ฮป h x, (h x).symmโŸฉ, -end +def is_positive (T : V โ†’โ‚—[โ„‚] V) : Prop := +โˆ€ x : V, 0 โ‰ค โŸชx, T xโŸซ_โ„‚.re โˆง (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ +-- def is_positive (T : V โ†’โ‚—[โ„‚] V) : Prop := (0 : V โ†’ โ„‚) โ‰ค ฮป x, โŸชx, T xโŸซ_โ„‚ +set_option max_memory 7070 /-- if `T.is_positive`, then `T.is_self_adjoint` and all its eigenvalues are non-negative -/ -lemma is_positive.self_adjoint_and_nonneg_spectrum [finite_dimensional โ„‚ V] +@[simp] lemma is_positive.self_adjoint_and_nonneg_spectrum [finite_dimensional โ„‚ V] (T : V โ†’โ‚—[โ„‚] V) (h : T.is_positive) : is_self_adjoint T โˆง โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = ฮผ.re โˆง 0 โ‰ค ฮผ.re := begin @@ -164,18 +158,18 @@ begin rw [โ† right, complex.of_real_re, complex.of_real_im] at this, rw [linear_map.sub_apply, inner_sub_left, โ† inner_conj_sym, linear_map.adjoint_inner_left, โ† right, is_R_or_C.conj_of_real, sub_self], }, - refine โŸจfrs,_โŸฉ, - intros ฮผ hฮผ, - rw โ† module.End.has_eigenvalue_iff_mem_spectrum at hฮผ, - have realeigen := (complex.eq_conj_iff_re.mp - (linear_map.is_symmetric.conj_eigenvalue_eq_self - ((linear_map.is_symmetric_iff_is_self_adjoint T).mpr frs) hฮผ)).symm, - refine โŸจrealeigen, _โŸฉ, - have hฮฑ : โˆƒ ฮฑ : โ„, ฮฑ = ฮผ.re := by use ฮผ.re, - cases hฮฑ with ฮฑ hฮฑ, - rw โ† hฮฑ, - rw [realeigen, โ† hฮฑ] at hฮผ, - exact eigenvalue_nonneg_of_nonneg hฮผ (ฮป x, ge_iff_le.mp (h x).1), + refine โŸจfrs,_โŸฉ, + intros ฮผ hฮผ, + rw โ† module.End.has_eigenvalue_iff_mem_spectrum at hฮผ, + have realeigen := (complex.eq_conj_iff_re.mp + (linear_map.is_symmetric.conj_eigenvalue_eq_self + ((linear_map.is_symmetric_iff_is_self_adjoint T).mpr frs) hฮผ)).symm, + refine โŸจrealeigen, _โŸฉ, + have hฮฑ : โˆƒ ฮฑ : โ„, ฮฑ = ฮผ.re := by use ฮผ.re, + cases hฮฑ with ฮฑ hฮฑ, + rw โ† hฮฑ, + rw [realeigen, โ† hฮฑ] at hฮผ, + exact eigenvalue_nonneg_of_nonneg hฮผ (ฮป x, ge_iff_le.mp (h x).1), end variables [finite_dimensional โ„‚ V] {n : โ„•} (hn : finite_dimensional.finrank โ„‚ V = n) @@ -215,43 +209,51 @@ noncomputable def sqrt (hT : T.is_symmetric) : V โ†’โ‚—[โ„‚] V := โ† mul_assoc, mul_comm] } lemma sqrt_eq (hT : T.is_symmetric) (v : V) : (T.sqrt hn hT) v = โˆ‘ (i : (fin n)), - real.sqrt (hT.eigenvalues hn i) โ€ข โŸช(hT.eigenvector_basis hn) i, vโŸซ_โ„‚ - โ€ข (hT.eigenvector_basis hn) i := rfl + real.sqrt (hT.eigenvalues hn i) โ€ข โŸชe hT hn i, vโŸซ_โ„‚ โ€ข e hT hn i := rfl -/-- `T.sqrt ^ 2 = T` and `T.sqrt.is_positive` -/ -lemma sqrt_sq_eq_linear_map_and_is_positive (hT : T.is_symmetric) +/-- the square root of a positive operator squared equals the operator -/ +@[simp] lemma sqrt_sq_eq (hT : T.is_symmetric) (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) : - (T.sqrt hn hT)^2 = T โˆง (T.sqrt hn hT).is_positive := + (T.sqrt hn hT)^2 = T := begin rw [pow_two, mul_eq_comp], + ext v, + simp only [comp_apply, linear_map.sqrt_eq, inner_sum, inner_smul_real_right], + simp only [โ† complex.coe_smul, smul_smul, inner_smul_right], + simp only [โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, + euclidean_space.single_apply, mul_boole, finset.sum_ite_eq, + finset.mem_univ, if_true, โ† smul_smul, complex.coe_smul], + symmetry, + simp only [orthonormal_basis.repr_apply_apply], + exact linear_map.of_pos_eq_sqrt_sqrt hn T hT hT1 v, +end + +/-- the square root of a positive operator is positive -/ +@[simp] lemma sqrt_is_positive (hT : T.is_symmetric) + (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) : + (T.sqrt hn hT).is_positive := +begin + intros x, + -- simp only [pi.zero_apply], split, - { ext v, - simp only [comp_apply, linear_map.sqrt_eq, inner_sum, inner_smul_real_right], - simp only [โ† complex.coe_smul, smul_smul, inner_smul_right], - simp only [โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, - euclidean_space.single_apply, mul_boole, finset.sum_ite_eq, - finset.mem_univ, if_true, โ† smul_smul, complex.coe_smul], - symmetry, - simp only [orthonormal_basis.repr_apply_apply], - exact linear_map.of_pos_eq_sqrt_sqrt hn T hT hT1 v, }, - { intro, - split, - { simp_rw [linear_map.sqrt_eq, inner_sum, โ† complex.coe_smul, smul_smul, inner_smul_right, - complex.re_sum, mul_assoc, mul_comm, โ† complex.real_smul, โ† inner_conj_sym x, - โ† complex.norm_sq_eq_conj_mul_self, complex.smul_re, complex.of_real_re, - smul_eq_mul], - apply finset.sum_nonneg', - intros i, - specialize hT1 (hT.eigenvalues hn i), - simp only [complex.of_real_re, eq_self_iff_true, true_and] at hT1, - simp_rw [mul_nonneg_iff, real.sqrt_nonneg, complex.norm_sq_nonneg, and_self, true_or], }, - { suffices : โˆ€ x, (star_ring_end โ„‚) โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚ = โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚, - { rw [โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re], - exact this x, }, - intro x, - simp_rw [inner_conj_sym, linear_map.sqrt_eq, sum_inner, inner_sum, โ† complex.coe_smul, - smul_smul, inner_smul_left, inner_smul_right, map_mul, is_R_or_C.conj_of_real, - inner_conj_sym, mul_assoc, mul_comm โŸช_, xโŸซ_โ„‚], }, }, + { simp_rw [linear_map.sqrt_eq, inner_sum, โ† complex.coe_smul, smul_smul, inner_smul_right, + complex.re_sum, mul_assoc, mul_comm, โ† complex.real_smul, โ† inner_conj_sym x, + โ† complex.norm_sq_eq_conj_mul_self, complex.smul_re, complex.of_real_re, + smul_eq_mul], + apply finset.sum_nonneg', + intros i, + specialize hT1 (hT.eigenvalues hn i), + simp only [complex.of_real_re, eq_self_iff_true, true_and] at hT1, + simp_rw [mul_nonneg_iff, real.sqrt_nonneg, complex.norm_sq_nonneg, and_self, true_or], }, + { suffices : โˆ€ x, (star_ring_end โ„‚) โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚ = โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚, + { + simp_rw is_R_or_C.eq_conj_iff_re at this, + simp only [pi.zero_apply, complex.zero_im, โ† is_R_or_C.im_eq_complex_im], + rw [โ† this], refl, }, + intro x, + simp_rw [inner_conj_sym, linear_map.sqrt_eq, sum_inner, inner_sum, โ† complex.coe_smul, + smul_smul, inner_smul_left, inner_smul_right, map_mul, is_R_or_C.conj_of_real, + inner_conj_sym, mul_assoc, mul_comm โŸช_, xโŸซ_โ„‚], }, end /-- `T.is_positive` if and only if `T.is_self_adjoint` and all its eigenvalues are nonnegative. -/ @@ -262,18 +264,18 @@ begin { intro h, exact linear_map.is_positive.self_adjoint_and_nonneg_spectrum T h, }, { intro h, have hT : T.is_symmetric := (is_symmetric_iff_is_self_adjoint T).mpr h.1, - rw [โ† (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT h.2).1, pow_two], + rw [โ† (linear_map.sqrt_sq_eq hn T hT h.2), pow_two], have : (T.sqrt hn hT) * (T.sqrt hn hT) = (T.sqrt hn hT).adjoint * (T.sqrt hn hT) := - by rw is_self_adjoint_iff'.mp (linear_map.is_positive.self_adjoint_and_nonneg_spectrum _ - (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT h.2).2).1, + by rw is_self_adjoint_iff'.mp + (is_positive.self_adjoint_and_nonneg_spectrum _ (T.sqrt_is_positive hn hT h.2)).1, rw this, clear this, intro, simp_rw [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K], - norm_cast, refine โŸจsq_nonneg โ€–(linear_map.sqrt hn T hT) xโ€–, rflโŸฉ, }, + norm_cast, refine โŸจsq_nonneg โ€–(linear_map.sqrt hn T hT) _โ€–, rflโŸฉ, }, end /-- every positive linear map can be written as `S.adjoint * S` for some linear map `S` -/ -lemma is_positive_iff_exists_linear_map_mul_adjoint : +lemma is_positive_iff_exists_adjoint_mul_self : T.is_positive โ†” โˆƒ S : V โ†’โ‚—[โ„‚] V, T = S.adjoint * S := begin split, @@ -282,15 +284,14 @@ begin rintro โŸจhT, hT1โŸฉ, use T.sqrt hn hT, rw [is_self_adjoint_iff'.mp (linear_map.is_positive.self_adjoint_and_nonneg_spectrum _ - (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT hT1).2).1, - โ† pow_two, (linear_map.sqrt_sq_eq_linear_map_and_is_positive hn T hT hT1).1], }, + (T.sqrt_is_positive hn hT hT1)).1, + โ† pow_two, (T.sqrt_sq_eq hn hT hT1)], }, { intros h x, cases h with S hS, simp_rw [hS, mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K], norm_cast, - refine โŸจsq_nonneg _, rflโŸฉ, }, + exact โŸจsq_nonneg _, rflโŸฉ, }, end - end linear_map section finite_dimensional @@ -298,26 +299,26 @@ section finite_dimensional variables (V : Type*) [inner_product_space โ„‚ V] [finite_dimensional โ„‚ V] (T : V โ†’L[โ„‚] V) open linear_map -lemma self_adjoint_clm_iff_self_adjoint_lm : - is_self_adjoint T โ†” is_self_adjoint T.to_linear_map := +@[simp] lemma continuous_linear_map.is_self_adjoint_to_linear_map : + is_self_adjoint T.to_linear_map โ†” is_self_adjoint T := begin simp_rw [continuous_linear_map.to_linear_map_eq_coe, is_self_adjoint_iff', continuous_linear_map.is_self_adjoint_iff', continuous_linear_map.ext_iff, linear_map.ext_iff, continuous_linear_map.coe_coe, adjoint_eq_to_clm_adjoint], - split, - { intros h x, rw โ† h x, refl, }, - { intros h x, rw โ† h x, refl, }, + refl, end -lemma is_positive_clm_iff_is_positive_lm : - T.is_positive โ†” linear_map.is_positive T.to_linear_map := +open_locale complex_order +@[simp] lemma continuous_linear_map.is_positive_to_linear_map : + T.to_linear_map.is_positive โ†” T.is_positive := begin simp_rw [linear_map.is_positive, continuous_linear_map.is_positive, - self_adjoint_clm_iff_self_adjoint_lm, linear_map.is_self_adjoint_iff_real_inner, + โ† continuous_linear_map.is_self_adjoint_to_linear_map, + โ† is_symmetric_iff_is_self_adjoint, + linear_map.is_symmetric_iff_real_inner, continuous_linear_map.re_apply_inner_self_apply, inner_re_symm, is_R_or_C.re_eq_complex_re, continuous_linear_map.to_linear_map_eq_coe, - continuous_linear_map.coe_coe, and.comm], - refine โŸจฮป h x, โŸจh.1 x, h.2 xโŸฉ, ฮป h, โŸจฮป x, (h x).1, ฮป x, (h x).2โŸฉโŸฉ, + continuous_linear_map.coe_coe, and.comm, โ† forall_and_distrib], end end finite_dimensional diff --git a/src/analysis/inner_product_space/symmetric.lean b/src/analysis/inner_product_space/symmetric.lean index 236b19b900c36..56019c3e5c434 100644 --- a/src/analysis/inner_product_space/symmetric.lean +++ b/src/analysis/inner_product_space/symmetric.lean @@ -150,6 +150,15 @@ begin ring }, end +lemma is_symmetric_iff_real_inner (T : V โ†’โ‚—[โ„‚] V) : + is_symmetric T โ†” โˆ€ x, (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ := +begin + simp_rw [is_symmetric_iff_inner_map_self_real, + inner_conj_sym, โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re, + inner_conj_sym], + exact โŸจฮป h x, (h x).symm, ฮป h x, (h x).symmโŸฉ, +end + end complex end linear_map From bcafe443fce210325a7e157236e14e6ec6420e03 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 29 Jan 2023 20:27:45 +0000 Subject: [PATCH 3/9] changes after review --- .../inner_product_space/positive.lean | 520 +++++++++++------- 1 file changed, 318 insertions(+), 202 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index 91b94805341e4..cb10a0aef1277 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -14,11 +14,20 @@ of requiring self adjointness in the definition. ## Main definitions +for linear maps: +* `is_positive` : a linear map is positive if it is symmetric and `โˆ€ x, 0 โ‰ค re โŸชT x, xโŸซ` + +for continuous linear maps: * `is_positive` : a continuous linear map is positive if it is self adjoint and `โˆ€ x, 0 โ‰ค re โŸชT x, xโŸซ` ## Main statements +for linear maps: +* `linear_map.is_positive.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. + +for continuous linear maps: * `continuous_linear_map.is_positive.conj_adjoint` : if `T : E โ†’L[๐•œ] E` is positive, then for any `S : E โ†’L[๐•œ] F`, `S โˆ˜L T โˆ˜L Sโ€ ` is also positive. * `continuous_linear_map.is_positive_iff_complex` : in a ***complex*** hilbert space, @@ -33,22 +42,325 @@ of requiring self adjointness in the definition. Positive operator -/ +open inner_product_space is_R_or_C +open_locale inner_product complex_conjugate +variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] +local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y -namespace continuous_linear_map +/-- `U` is **pairwise orthogonal** to `V` if for all `u โˆˆ U` and for all `v โˆˆ V` +we get `โŸชu, vโŸซ = 0` -/ +def submodule.pairwise_orthogonal (U V : submodule ๐•œ E) : Prop := +โˆ€ u : U, โˆ€ v : V, โŸช(u : E), (v : E)โŸซ = 0 -open inner_product_space is_R_or_C continuous_linear_map -open_locale inner_product complex_conjugate +/-- `U` is pairwise orthogonal to `Uแ—ฎ` -/ +lemma submodule.orthogonal_is_pairwise_orthogonal (U : submodule ๐•œ E) : + U.pairwise_orthogonal Uแ—ฎ := +ฮป u v, (set_like.coe_mem v) u (set_like.coe_mem u) + +/-- `U` is pairwise orthogonal to `V` if and only if `V` is pairwise +orthogonal to `U` -/ +lemma submodule.pairwise_orthogonal_symm_iff (U V : submodule ๐•œ E) : + U.pairwise_orthogonal V โ†” V.pairwise_orthogonal U := +begin + simp_rw [submodule.pairwise_orthogonal, inner_eq_zero_sym], + rw forall_swap, +end +namespace linear_map -variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] - [complete_space E] [complete_space F] -local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y +/-- `T` is (semi-definite) **positive** if `T` is symmetric +and `โˆ€ x : V, 0 โ‰ค re โŸชx, T xโŸซ` -/ +def is_positive (T : E โ†’โ‚—[๐•œ] E) : Prop := +T.is_symmetric โˆง โˆ€ x : E, 0 โ‰ค re โŸชx, T xโŸซ + +lemma is_positive_zero : (0 : E โ†’โ‚—[๐•œ] E).is_positive := +begin + refine โŸจis_symmetric_zero, ฮป x, _โŸฉ, + simp_rw [zero_apply, inner_re_zero_right], +end + +lemma is_positive_one : (1 : E โ†’โ‚—[๐•œ] E).is_positive := +โŸจis_symmetric_id, ฮป x, inner_self_nonnegโŸฉ + +lemma is_positive.add {S T : E โ†’โ‚—[๐•œ] E} (hS : S.is_positive) (hT : T.is_positive) : + (S + T).is_positive := +begin + refine โŸจis_symmetric.add hS.1 hT.1, ฮป x, _โŸฉ, + rw [add_apply, inner_add_right, map_add], + exact add_nonneg (hS.2 _) (hT.2 _), +end + +lemma is_positive.inner_nonneg_left {T : E โ†’โ‚—[๐•œ] E} (hT : is_positive T) (x : E) : + 0 โ‰ค re โŸชT x, xโŸซ := +by { rw inner_re_symm, exact hT.2 x, } + +lemma is_positive.inner_nonneg_right {T : E โ†’โ‚—[๐•œ] E} (hT : is_positive T) (x : E) : + 0 โ‰ค re โŸชx, T xโŸซ := +hT.2 x + +/-- a linear projection onto `U` along its complement `V` is positive if +and only if `U` and `V` are pairwise orthogonal -/ +lemma linear_proj_is_positive_iff {U V : submodule ๐•œ E} (hUV : is_compl U V) : + (U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_positive โ†” U.pairwise_orthogonal V := +begin + split, + { intros h u v, + rw [โ† submodule.linear_proj_of_is_compl_apply_left hUV u, + โ† submodule.subtype_apply _, โ† comp_apply, h.1 _ _, + comp_apply, submodule.linear_proj_of_is_compl_apply_right hUV v, + map_zero, inner_zero_right], }, + { intro h, + have : (U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_symmetric, + { intros x y, + nth_rewrite 0 โ† submodule.linear_proj_add_linear_proj_of_is_compl_eq_self hUV y, + nth_rewrite 1 โ† submodule.linear_proj_add_linear_proj_of_is_compl_eq_self hUV x, + simp_rw [inner_add_right, inner_add_left, comp_apply, + submodule.subtype_apply _, h _ _, inner_eq_zero_sym.mp (h _ _)], }, + refine โŸจthis, _โŸฉ, + intros x, + rw [comp_apply, submodule.subtype_apply, + โ† submodule.linear_proj_of_is_compl_idempotent, + โ† submodule.subtype_apply, โ† comp_apply, + โ† this _ ((U.linear_proj_of_is_compl V hUV) x)], + exact inner_self_nonneg, }, +end + +/-- set over `๐•œ` is **non-negative** if all its elements are real and non-negative -/ +def set.is_nonneg (A : set ๐•œ) : Prop := +โˆ€ x : ๐•œ, x โˆˆ A โ†’ โ†‘(re x) = x โˆง 0 โ‰ค re x + +section finite_dimensional + +local notation `e` := is_symmetric.eigenvector_basis +local notation `ฮฑ` := is_symmetric.eigenvalues +local notation `โˆš` := real.sqrt + +variables {n : โ„•} [decidable_eq ๐•œ] [finite_dimensional ๐•œ E] (T : E โ†’โ‚—[๐•œ] E) + +/-- the spectrum of a positive linear map is non-negative -/ +lemma is_positive.nonneg_spectrum (h : T.is_positive) : + (spectrum ๐•œ T).is_nonneg := +begin + cases h with hT h, + intros ฮผ hฮผ, + simp_rw [โ† module.End.has_eigenvalue_iff_mem_spectrum] at hฮผ, + have : โ†‘(re ฮผ) = ฮผ, + { simp_rw [โ† eq_conj_iff_re], + exact is_symmetric.conj_eigenvalue_eq_self hT hฮผ, }, + rw โ† this at hฮผ, + exact โŸจthis, eigenvalue_nonneg_of_nonneg hฮผ hโŸฉ, +end + +open_locale big_operators +/-- 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`) -/ +lemma sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum + (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) + (hT1 : (spectrum ๐•œ T).is_nonneg) (v : E) : + T v = โˆ‘ i, ((โˆš (ฮฑ hT hn i) โ€ข โˆš (ฮฑ hT hn i)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := +begin + have : โˆ€ i : fin n, 0 โ‰ค ฮฑ hT hn i := ฮป i, + by { specialize hT1 (hT.eigenvalues hn i), + simp only [of_real_re, eq_self_iff_true, true_and] at hT1, + apply hT1 (module.End.mem_spectrum_of_has_eigenvalue + (is_symmetric.has_eigenvalue_eigenvalues hT hn i)), }, + calc T v = โˆ‘ i, โŸชe hT hn i, vโŸซ โ€ข T (e hT hn i) : _ + ... = โˆ‘ i, ((โˆš (ฮฑ hT hn i) โ€ข โˆš (ฮฑ hT hn i)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข (e hT hn i) : _, + simp_rw [โ† orthonormal_basis.repr_apply_apply, โ† map_smul_of_tower, โ† linear_map.map_sum, + orthonormal_basis.sum_repr (e hT hn) v, is_symmetric.apply_eigenvector_basis, + smul_smul, of_real_smul, โ† of_real_mul, โ† real.sqrt_mul (this _), + real.sqrt_mul_self (this _), mul_comm], +end + +/-- given a symmetric linear map `T` and a real number `r`, +we can define a linear map `S` such that `S = T ^ r` -/ +noncomputable def re_pow (hn : finite_dimensional.finrank ๐•œ E = n) + (hT : T.is_symmetric) (r : โ„) : E โ†’โ‚—[๐•œ] E := +{ to_fun := ฮป v, โˆ‘ i : fin n, ((((ฮฑ hT hn i : โ„) ^ r : โ„)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i, + map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], + map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, + ring_hom.id_apply, smul_smul, โ† mul_assoc, mul_comm] } + +lemma re_pow_apply (hn : finite_dimensional.finrank ๐•œ E = n) + (hT : T.is_symmetric) (r : โ„) (v : E) : + T.re_pow hn hT r v = โˆ‘ i : fin n, (((ฮฑ hT hn i : โ„) ^ r : โ„) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := +rfl + +/-- the square root of a symmetric linear map can then directly be defined with `re_pow` -/ +noncomputable def sqrt (hn : finite_dimensional.finrank ๐•œ E = n) (h : T.is_symmetric) : + E โ†’โ‚—[๐•œ] E := T.re_pow hn h (1 / 2 : โ„) + +/-- 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`) -/ +lemma sqrt_apply (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (x : E) : + T.sqrt hn hT x = โˆ‘ i, (โˆš (ฮฑ hT hn i) : ๐•œ) โ€ข โŸชe hT hn i, xโŸซ โ€ข e hT hn i := +by { simp_rw [real.sqrt_eq_rpow _], refl } + +/-- 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` -/ +lemma sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum + (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) + (hT1 : (spectrum ๐•œ T).is_nonneg) : + (T.sqrt hn hT) ^ 2 = T := +by simp_rw [pow_two, mul_eq_comp, linear_map.ext_iff, comp_apply, sqrt_apply, + inner_sum, inner_smul_real_right, smul_smul, inner_smul_right, + โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, + euclidean_space.single_apply, mul_boole, smul_ite, smul_zero, + finset.sum_ite_eq, finset.mem_univ, if_true, algebra.mul_smul_comm, + sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1, + orthonormal_basis.repr_apply_apply, โ† smul_eq_mul, โ† smul_assoc, + eq_self_iff_true, forall_const] + +/-- given a symmetric linear map `T`, we have that its root is positive -/ +lemma is_symmetric.sqrt_is_positive + (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) : + (T.sqrt hn hT).is_positive := +begin + have : (T.sqrt hn hT).is_symmetric, + { intros x y, + simp_rw [sqrt_apply T hn hT, inner_sum, sum_inner, smul_smul, inner_smul_right, + inner_smul_left], + have : โˆ€ i : fin n, conj ((โˆš (ฮฑ hT hn i)) : ๐•œ) = ((โˆš (ฮฑ hT hn i)) : ๐•œ) := ฮป i, + by simp_rw [eq_conj_iff_re, of_real_re], + simp_rw [mul_assoc, map_mul, this _, inner_conj_sym, + mul_comm โŸชe hT hn _, yโŸซ _, โ† mul_assoc], }, + refine โŸจthis, _โŸฉ, + intro x, + simp_rw [sqrt_apply _ hn hT, inner_sum, add_monoid_hom.map_sum, inner_smul_right], + apply finset.sum_nonneg', + intros i, + simp_rw [โ† inner_conj_sym x _, โ† orthonormal_basis.repr_apply_apply, + mul_conj, โ† of_real_mul, of_real_re], + exact mul_nonneg (real.sqrt_nonneg _) (norm_sq_nonneg _), +end + +/-- `T` is positive if and only if `T` is symmetric +(which is automatic from the definition of positivity) +and has a non-negative spectrum -/ +lemma is_positive_iff_is_symmetric_and_nonneg_spectrum + (hn : finite_dimensional.finrank ๐•œ E = n) : + T.is_positive โ†” T.is_symmetric โˆง (spectrum ๐•œ T).is_nonneg := +begin + refine โŸจฮป h, โŸจh.1, ฮป ฮผ hฮผ, is_positive.nonneg_spectrum T h ฮผ hฮผโŸฉ, + ฮป h, โŸจh.1, _โŸฉโŸฉ, + intros x, + rw [โ† sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn h.1 h.2, + pow_two, mul_apply, โ† adjoint_inner_left, + is_self_adjoint_iff'.mp + ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn h.1).1)], + exact inner_self_nonneg, +end + +/-- `T` is positive if and only if there exists a +linear map `S` such that `T = S.adjoint * S` -/ +lemma is_positive_iff_exists_adjoint_mul_self + (hn : finite_dimensional.finrank ๐•œ E = n) : + T.is_positive โ†” โˆƒ S : E โ†’โ‚—[๐•œ] E, T = S.adjoint * S := +begin + split, + { rw [is_positive_iff_is_symmetric_and_nonneg_spectrum T hn], + rintro โŸจhT, hT1โŸฉ, + use T.sqrt hn hT, + rw [is_self_adjoint_iff'.mp + ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn hT).1), + โ† pow_two], + exact (sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1).symm, }, + { intros h, + rcases h with โŸจS, rflโŸฉ, + refine โŸจis_symmetric_adjoint_mul_self S, _โŸฉ, + intro x, + simp_rw [mul_apply, adjoint_inner_right], + exact inner_self_nonneg, }, +end + +section complex + +/-- for spaces `V` over `โ„‚`, it suffices to define positivity with +`0 โ‰ค โŸชv, T vโŸซ_โ„‚` for all `v โˆˆ V` -/ +lemma complex_is_positive {V : Type*} [inner_product_space โ„‚ V] (T : V โ†’โ‚—[โ„‚] V) : + T.is_positive โ†” โˆ€ v : V, โ†‘(re โŸชv, T vโŸซ_โ„‚) = โŸชv, T vโŸซ_โ„‚ โˆง 0 โ‰ค re โŸชv, T vโŸซ_โ„‚ := +by simp_rw [is_positive, is_symmetric_iff_inner_map_self_real, inner_conj_sym, + โ† eq_conj_iff_re, inner_conj_sym, โ† forall_and_distrib, and_comm, eq_comm] + +end complex + +lemma is_positive.conj_adjoint [finite_dimensional ๐•œ F] + (T : E โ†’โ‚—[๐•œ] E) (S : E โ†’โ‚—[๐•œ] F) (h : T.is_positive) : + (S.comp (T.comp S.adjoint)).is_positive := +begin + split, + intros u v, + simp_rw [comp_apply, โ† adjoint_inner_left _ (T _), โ† adjoint_inner_right _ (T _) _], + exact h.1 _ _, + intros v, + simp_rw [comp_apply, โ† adjoint_inner_left _ (T _)], + exact h.2 _, +end + +lemma is_positive.adjoint_conj [finite_dimensional ๐•œ F] + (T : E โ†’โ‚—[๐•œ] E) (S : F โ†’โ‚—[๐•œ] E) (h : T.is_positive) : + (S.adjoint.comp (T.comp S)).is_positive := +begin + split, + intros u v, + simp_rw [comp_apply, adjoint_inner_left, adjoint_inner_right], + exact h.1 _ _, + intros v, + simp_rw [comp_apply, adjoint_inner_right], + exact h.2 _, +end + +variable (hn : finite_dimensional.finrank ๐•œ E = n) +local notation `โˆšTโ‹†`T := (T.adjoint.comp T).sqrt hn (is_symmetric_adjoint_mul_self T) + +/-- we have `(T.adjoint.comp T).sqrt` is positive, given any linear map `T` -/ +lemma sqrt_adjoint_self_is_positive (T : E โ†’โ‚—[๐•œ] E) : (โˆšTโ‹†T).is_positive := +is_symmetric.sqrt_is_positive _ hn (is_symmetric_adjoint_mul_self T) + +/-- given any linear map `T` and `x โˆˆ E` we have +`โ€–(T.adjoint.comp T).sqrt xโ€– = โ€–T xโ€–` -/ +lemma norm_of_sqrt_adjoint_mul_self_eq (T : E โ†’โ‚—[๐•œ] E) (x : E) : + โ€–(โˆšTโ‹†T) xโ€– = โ€–T xโ€– := +begin +simp_rw [โ† sq_eq_sq (norm_nonneg _) (norm_nonneg _), + โ† inner_self_eq_norm_sq, โ† adjoint_inner_left, + is_self_adjoint_iff'.mp + ((is_symmetric_iff_is_self_adjoint _).mp (sqrt_adjoint_self_is_positive hn T).1), + โ† mul_eq_comp, โ† mul_apply, โ† pow_two, mul_eq_comp], + congr, + apply sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum, + apply is_positive.nonneg_spectrum _ โŸจis_symmetric_adjoint_mul_self T, _โŸฉ, + intros x, + simp_rw [mul_apply, adjoint_inner_right], + exact inner_self_nonneg, +end + +end finite_dimensional + +end linear_map + + +namespace continuous_linear_map + +open continuous_linear_map + +variables [complete_space E] [complete_space F] /-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is self adjoint and `โˆ€ x, 0 โ‰ค re โŸชT x, xโŸซ`. -/ def is_positive (T : E โ†’L[๐•œ] E) : Prop := is_self_adjoint T โˆง โˆ€ x, 0 โ‰ค T.re_apply_inner_self x +lemma is_positive.to_linear_map (T : E โ†’L[๐•œ] E) : + T.to_linear_map.is_positive โ†” T.is_positive := +by simp_rw [to_linear_map_eq_coe, linear_map.is_positive, continuous_linear_map.coe_coe, + is_positive, is_self_adjoint_iff_is_symmetric, re_apply_inner_self_apply T, + inner_re_symm] + lemma is_positive.is_self_adjoint {T : E โ†’L[๐•œ] E} (hT : is_positive T) : is_self_adjoint T := hT.1 @@ -126,199 +438,3 @@ end end complex end continuous_linear_map - -namespace linear_map - -open linear_map - -variables {V ๐•œ : Type*} [is_R_or_C ๐•œ] [inner_product_space โ„‚ V] -open_locale inner_product complex_conjugate big_operators --complex_order -open is_R_or_C -local notation `e` := is_symmetric.eigenvector_basis -local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y - -/-- `T` is (semi-definite) positive if `โˆ€ x : V, โŸชx, T xโŸซ_โ„‚ โ‰ฅ 0` -/ -def is_positive (T : V โ†’โ‚—[โ„‚] V) : Prop := -โˆ€ x : V, 0 โ‰ค โŸชx, T xโŸซ_โ„‚.re โˆง (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ --- def is_positive (T : V โ†’โ‚—[โ„‚] V) : Prop := (0 : V โ†’ โ„‚) โ‰ค ฮป x, โŸชx, T xโŸซ_โ„‚ - -set_option max_memory 7070 -/-- if `T.is_positive`, then `T.is_self_adjoint` and all its eigenvalues are non-negative -/ -@[simp] lemma is_positive.self_adjoint_and_nonneg_spectrum [finite_dimensional โ„‚ V] - (T : V โ†’โ‚—[โ„‚] V) (h : T.is_positive) : - is_self_adjoint T โˆง โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = ฮผ.re โˆง 0 โ‰ค ฮผ.re := -begin - have frs : is_self_adjoint T, - { rw linear_map.is_self_adjoint_iff', - symmetry, - rw [โ† sub_eq_zero, โ† inner_map_self_eq_zero], - intro x, - cases h x, - have := complex.re_add_im (inner x (T x)), - rw [โ† right, complex.of_real_re, complex.of_real_im] at this, - rw [linear_map.sub_apply, inner_sub_left, โ† inner_conj_sym, linear_map.adjoint_inner_left, - โ† right, is_R_or_C.conj_of_real, sub_self], }, - refine โŸจfrs,_โŸฉ, - intros ฮผ hฮผ, - rw โ† module.End.has_eigenvalue_iff_mem_spectrum at hฮผ, - have realeigen := (complex.eq_conj_iff_re.mp - (linear_map.is_symmetric.conj_eigenvalue_eq_self - ((linear_map.is_symmetric_iff_is_self_adjoint T).mpr frs) hฮผ)).symm, - refine โŸจrealeigen, _โŸฉ, - have hฮฑ : โˆƒ ฮฑ : โ„, ฮฑ = ฮผ.re := by use ฮผ.re, - cases hฮฑ with ฮฑ hฮฑ, - rw โ† hฮฑ, - rw [realeigen, โ† hฮฑ] at hฮผ, - exact eigenvalue_nonneg_of_nonneg hฮผ (ฮป x, ge_iff_le.mp (h x).1), -end - -variables [finite_dimensional โ„‚ V] {n : โ„•} (hn : finite_dimensional.finrank โ„‚ V = n) -variables (T : V โ†’โ‚—[โ„‚] V) - -lemma of_pos_eq_sqrt_sqrt (hT : T.is_symmetric) - (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) (v : V) : - T v = โˆ‘ (i : (fin n)), real.sqrt (hT.eigenvalues hn i) โ€ข real.sqrt (hT.eigenvalues hn i) - โ€ข โŸช(e hT hn) i, vโŸซ_โ„‚ โ€ข (e hT hn) i := -begin - have : โˆ€ i : fin n, 0 โ‰ค hT.eigenvalues hn i := ฮป i, - by { specialize hT1 (hT.eigenvalues hn i), - simp only [complex.of_real_re, eq_self_iff_true, true_and] at hT1, - apply hT1 (module.End.mem_spectrum_of_has_eigenvalue - (is_symmetric.has_eigenvalue_eigenvalues hT hn i)), }, - calc T v = โˆ‘ (i : (fin n)), โŸช(e hT hn) i, vโŸซ_โ„‚ โ€ข T ((e hT hn) i) : - by simp_rw [โ† orthonormal_basis.repr_apply_apply, โ† map_smul_of_tower, โ† linear_map.map_sum, - orthonormal_basis.sum_repr (is_symmetric.eigenvector_basis hT hn) v] - ... = โˆ‘ (i : (fin n)), - real.sqrt (hT.eigenvalues hn i) โ€ข real.sqrt (hT.eigenvalues hn i) โ€ข - โŸช(e hT hn) i, vโŸซ_โ„‚ โ€ข (e hT hn) i : - by simp_rw [is_symmetric.apply_eigenvector_basis, smul_smul, โ† real.sqrt_mul (this _), - real.sqrt_mul_self (this _), mul_comm, โ† smul_smul, complex.coe_smul], -end - -include hn -/-- Let `e = hT.eigenvector_basis hn` so that we have `T (e i) = ฮฑ i โ€ข e i` for each `i`. -Then when `T.is_symmetric` and all its eigenvalues are nonnegative, -we can define `T.sqrt` by `e i โ†ฆ โˆšฮฑ i โ€ข e i`. -/ -noncomputable def sqrt (hT : T.is_symmetric) : V โ†’โ‚—[โ„‚] V := -{ to_fun := ฮป v, โˆ‘ (i : (fin n)), - real.sqrt (hT.eigenvalues hn i) โ€ข โŸช(hT.eigenvector_basis hn) i, vโŸซ_โ„‚ - โ€ข (hT.eigenvector_basis hn) i, - map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], - map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, - ring_hom.id_apply, โ† complex.coe_smul, smul_smul, - โ† mul_assoc, mul_comm] } - -lemma sqrt_eq (hT : T.is_symmetric) (v : V) : (T.sqrt hn hT) v = โˆ‘ (i : (fin n)), - real.sqrt (hT.eigenvalues hn i) โ€ข โŸชe hT hn i, vโŸซ_โ„‚ โ€ข e hT hn i := rfl - -/-- the square root of a positive operator squared equals the operator -/ -@[simp] lemma sqrt_sq_eq (hT : T.is_symmetric) - (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) : - (T.sqrt hn hT)^2 = T := -begin - rw [pow_two, mul_eq_comp], - ext v, - simp only [comp_apply, linear_map.sqrt_eq, inner_sum, inner_smul_real_right], - simp only [โ† complex.coe_smul, smul_smul, inner_smul_right], - simp only [โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, - euclidean_space.single_apply, mul_boole, finset.sum_ite_eq, - finset.mem_univ, if_true, โ† smul_smul, complex.coe_smul], - symmetry, - simp only [orthonormal_basis.repr_apply_apply], - exact linear_map.of_pos_eq_sqrt_sqrt hn T hT hT1 v, -end - -/-- the square root of a positive operator is positive -/ -@[simp] lemma sqrt_is_positive (hT : T.is_symmetric) - (hT1 : โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) : - (T.sqrt hn hT).is_positive := -begin - intros x, - -- simp only [pi.zero_apply], - split, - { simp_rw [linear_map.sqrt_eq, inner_sum, โ† complex.coe_smul, smul_smul, inner_smul_right, - complex.re_sum, mul_assoc, mul_comm, โ† complex.real_smul, โ† inner_conj_sym x, - โ† complex.norm_sq_eq_conj_mul_self, complex.smul_re, complex.of_real_re, - smul_eq_mul], - apply finset.sum_nonneg', - intros i, - specialize hT1 (hT.eigenvalues hn i), - simp only [complex.of_real_re, eq_self_iff_true, true_and] at hT1, - simp_rw [mul_nonneg_iff, real.sqrt_nonneg, complex.norm_sq_nonneg, and_self, true_or], }, - { suffices : โˆ€ x, (star_ring_end โ„‚) โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚ = โŸชx, (T.sqrt hn hT) xโŸซ_โ„‚, - { - simp_rw is_R_or_C.eq_conj_iff_re at this, - simp only [pi.zero_apply, complex.zero_im, โ† is_R_or_C.im_eq_complex_im], - rw [โ† this], refl, }, - intro x, - simp_rw [inner_conj_sym, linear_map.sqrt_eq, sum_inner, inner_sum, โ† complex.coe_smul, - smul_smul, inner_smul_left, inner_smul_right, map_mul, is_R_or_C.conj_of_real, - inner_conj_sym, mul_assoc, mul_comm โŸช_, xโŸซ_โ„‚], }, -end - -/-- `T.is_positive` if and only if `T.is_self_adjoint` and all its eigenvalues are nonnegative. -/ -theorem is_positive_iff_self_adjoint_and_nonneg_eigenvalues : - T.is_positive โ†” is_self_adjoint T โˆง (โˆ€ ฮผ : โ„‚, ฮผ โˆˆ spectrum โ„‚ T โ†’ ฮผ = โ†‘ฮผ.re โˆง 0 โ‰ค ฮผ.re) := -begin - split, - { intro h, exact linear_map.is_positive.self_adjoint_and_nonneg_spectrum T h, }, - { intro h, - have hT : T.is_symmetric := (is_symmetric_iff_is_self_adjoint T).mpr h.1, - rw [โ† (linear_map.sqrt_sq_eq hn T hT h.2), pow_two], - have : (T.sqrt hn hT) * (T.sqrt hn hT) = (T.sqrt hn hT).adjoint * (T.sqrt hn hT) := - by rw is_self_adjoint_iff'.mp - (is_positive.self_adjoint_and_nonneg_spectrum _ (T.sqrt_is_positive hn hT h.2)).1, - rw this, clear this, - intro, - simp_rw [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K], - norm_cast, refine โŸจsq_nonneg โ€–(linear_map.sqrt hn T hT) _โ€–, rflโŸฉ, }, -end - -/-- every positive linear map can be written as `S.adjoint * S` for some linear map `S` -/ -lemma is_positive_iff_exists_adjoint_mul_self : - T.is_positive โ†” โˆƒ S : V โ†’โ‚—[โ„‚] V, T = S.adjoint * S := -begin - split, - { rw [linear_map.is_positive_iff_self_adjoint_and_nonneg_eigenvalues hn, - โ† is_symmetric_iff_is_self_adjoint], - rintro โŸจhT, hT1โŸฉ, - use T.sqrt hn hT, - rw [is_self_adjoint_iff'.mp (linear_map.is_positive.self_adjoint_and_nonneg_spectrum _ - (T.sqrt_is_positive hn hT hT1)).1, - โ† pow_two, (T.sqrt_sq_eq hn hT hT1)], }, - { intros h x, - cases h with S hS, - simp_rw [hS, mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K], - norm_cast, - exact โŸจsq_nonneg _, rflโŸฉ, }, -end -end linear_map - -section finite_dimensional - -variables (V : Type*) [inner_product_space โ„‚ V] [finite_dimensional โ„‚ V] (T : V โ†’L[โ„‚] V) - -open linear_map -@[simp] lemma continuous_linear_map.is_self_adjoint_to_linear_map : - is_self_adjoint T.to_linear_map โ†” is_self_adjoint T := -begin - simp_rw [continuous_linear_map.to_linear_map_eq_coe, is_self_adjoint_iff', - continuous_linear_map.is_self_adjoint_iff', continuous_linear_map.ext_iff, - linear_map.ext_iff, continuous_linear_map.coe_coe, adjoint_eq_to_clm_adjoint], - refl, -end - -open_locale complex_order -@[simp] lemma continuous_linear_map.is_positive_to_linear_map : - T.to_linear_map.is_positive โ†” T.is_positive := -begin - simp_rw [linear_map.is_positive, continuous_linear_map.is_positive, - โ† continuous_linear_map.is_self_adjoint_to_linear_map, - โ† is_symmetric_iff_is_self_adjoint, - linear_map.is_symmetric_iff_real_inner, - continuous_linear_map.re_apply_inner_self_apply, inner_re_symm, - is_R_or_C.re_eq_complex_re, continuous_linear_map.to_linear_map_eq_coe, - continuous_linear_map.coe_coe, and.comm, โ† forall_and_distrib], -end - -end finite_dimensional From d0161f0fa0574420bbeb734d9fe32d0e097aefa5 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 30 Jan 2023 09:32:02 +0000 Subject: [PATCH 4/9] fix --- .../inner_product_space/positive.lean | 24 +++++++++++-------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index cb10a0aef1277..2d89678bf1438 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -135,7 +135,7 @@ local notation `e` := is_symmetric.eigenvector_basis local notation `ฮฑ` := is_symmetric.eigenvalues local notation `โˆš` := real.sqrt -variables {n : โ„•} [decidable_eq ๐•œ] [finite_dimensional ๐•œ E] (T : E โ†’โ‚—[๐•œ] E) +variables {n : โ„•} [finite_dimensional ๐•œ E] (T : E โ†’โ‚—[๐•œ] E) /-- the spectrum of a positive linear map is non-negative -/ lemma is_positive.nonneg_spectrum (h : T.is_positive) : @@ -157,7 +157,7 @@ we can write `T x = โˆ‘ i, โˆšฮฑ i โ€ข โˆšฮฑ i โ€ข โŸชe i, xโŸซ` for any `x โˆˆ where `ฮฑ i` are the eigenvalues of `T` and `e i` are the respective eigenvectors that form an eigenbasis (`is_symmetric.eigenvector_basis`) -/ lemma sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum - (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) + [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (hT1 : (spectrum ๐•œ T).is_nonneg) (v : E) : T v = โˆ‘ i, ((โˆš (ฮฑ hT hn i) โ€ข โˆš (ฮฑ hT hn i)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := begin @@ -176,34 +176,36 @@ end /-- given a symmetric linear map `T` and a real number `r`, we can define a linear map `S` such that `S = T ^ r` -/ -noncomputable def re_pow (hn : finite_dimensional.finrank ๐•œ E = n) +noncomputable def re_pow [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (r : โ„) : E โ†’โ‚—[๐•œ] E := { to_fun := ฮป v, โˆ‘ i : fin n, ((((ฮฑ hT hn i : โ„) ^ r : โ„)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i, map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, ring_hom.id_apply, smul_smul, โ† mul_assoc, mul_comm] } -lemma re_pow_apply (hn : finite_dimensional.finrank ๐•œ E = n) +lemma re_pow_apply [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (r : โ„) (v : E) : T.re_pow hn hT r v = โˆ‘ i : fin n, (((ฮฑ hT hn i : โ„) ^ r : โ„) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := rfl /-- the square root of a symmetric linear map can then directly be defined with `re_pow` -/ -noncomputable def sqrt (hn : finite_dimensional.finrank ๐•œ E = n) (h : T.is_symmetric) : +noncomputable def sqrt [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) + (h : T.is_symmetric) : E โ†’โ‚—[๐•œ] E := T.re_pow hn h (1 / 2 : โ„) /-- 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`) -/ -lemma sqrt_apply (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (x : E) : +lemma sqrt_apply (hn : finite_dimensional.finrank ๐•œ E = n) [decidable_eq ๐•œ] + (hT : T.is_symmetric) (x : E) : T.sqrt hn hT x = โˆ‘ i, (โˆš (ฮฑ hT hn i) : ๐•œ) โ€ข โŸชe hT hn i, xโŸซ โ€ข e hT hn i := by { simp_rw [real.sqrt_eq_rpow _], refl } /-- 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` -/ lemma sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum - (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) + [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (hT1 : (spectrum ๐•œ T).is_nonneg) : (T.sqrt hn hT) ^ 2 = T := by simp_rw [pow_two, mul_eq_comp, linear_map.ext_iff, comp_apply, sqrt_apply, @@ -217,7 +219,7 @@ by simp_rw [pow_two, mul_eq_comp, linear_map.ext_iff, comp_apply, sqrt_apply, /-- given a symmetric linear map `T`, we have that its root is positive -/ lemma is_symmetric.sqrt_is_positive - (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) : + [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) : (T.sqrt hn hT).is_positive := begin have : (T.sqrt hn hT).is_symmetric, @@ -245,6 +247,7 @@ lemma is_positive_iff_is_symmetric_and_nonneg_spectrum (hn : finite_dimensional.finrank ๐•œ E = n) : T.is_positive โ†” T.is_symmetric โˆง (spectrum ๐•œ T).is_nonneg := begin + classical, refine โŸจฮป h, โŸจh.1, ฮป ฮผ hฮผ, is_positive.nonneg_spectrum T h ฮผ hฮผโŸฉ, ฮป h, โŸจh.1, _โŸฉโŸฉ, intros x, @@ -261,6 +264,7 @@ lemma is_positive_iff_exists_adjoint_mul_self (hn : finite_dimensional.finrank ๐•œ E = n) : T.is_positive โ†” โˆƒ S : E โ†’โ‚—[๐•œ] E, T = S.adjoint * S := begin + classical, split, { rw [is_positive_iff_is_symmetric_and_nonneg_spectrum T hn], rintro โŸจhT, hT1โŸฉ, @@ -318,12 +322,12 @@ variable (hn : finite_dimensional.finrank ๐•œ E = n) local notation `โˆšTโ‹†`T := (T.adjoint.comp T).sqrt hn (is_symmetric_adjoint_mul_self T) /-- we have `(T.adjoint.comp T).sqrt` is positive, given any linear map `T` -/ -lemma sqrt_adjoint_self_is_positive (T : E โ†’โ‚—[๐•œ] E) : (โˆšTโ‹†T).is_positive := +lemma sqrt_adjoint_self_is_positive [decidable_eq ๐•œ] (T : E โ†’โ‚—[๐•œ] E) : (โˆšTโ‹†T).is_positive := is_symmetric.sqrt_is_positive _ hn (is_symmetric_adjoint_mul_self T) /-- given any linear map `T` and `x โˆˆ E` we have `โ€–(T.adjoint.comp T).sqrt xโ€– = โ€–T xโ€–` -/ -lemma norm_of_sqrt_adjoint_mul_self_eq (T : E โ†’โ‚—[๐•œ] E) (x : E) : +lemma norm_of_sqrt_adjoint_mul_self_eq [decidable_eq ๐•œ] (T : E โ†’โ‚—[๐•œ] E) (x : E) : โ€–(โˆšTโ‹†T) xโ€– = โ€–T xโ€– := begin simp_rw [โ† sq_eq_sq (norm_nonneg _) (norm_nonneg _), From 85b8249ebf96fc0a0e9af58fef8fc54c23c7d036 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 4 Apr 2023 18:28:56 +0000 Subject: [PATCH 5/9] delete pairwise_orthogonal --- .../inner_product_space/positive.lean | 23 ++----------------- 1 file changed, 2 insertions(+), 21 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index 3842e6e7d42c2..c2c7e69c07334 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -47,25 +47,6 @@ open_locale inner_product complex_conjugate variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y -/-- `U` is **pairwise orthogonal** to `V` if for all `u โˆˆ U` and for all `v โˆˆ V` -we get `โŸชu, vโŸซ = 0` -/ -def submodule.pairwise_orthogonal (U V : submodule ๐•œ E) : Prop := -โˆ€ u : U, โˆ€ v : V, โŸช(u : E), (v : E)โŸซ = 0 - -/-- `U` is pairwise orthogonal to `Uแ—ฎ` -/ -lemma submodule.orthogonal_is_pairwise_orthogonal (U : submodule ๐•œ E) : - U.pairwise_orthogonal Uแ—ฎ := -ฮป u v, (set_like.coe_mem v) u (set_like.coe_mem u) - -/-- `U` is pairwise orthogonal to `V` if and only if `V` is pairwise -orthogonal to `U` -/ -lemma submodule.pairwise_orthogonal_symm_iff (U V : submodule ๐•œ E) : - U.pairwise_orthogonal V โ†” V.pairwise_orthogonal U := -begin - simp_rw [submodule.pairwise_orthogonal, inner_eq_zero_sym], - rw forall_swap, -end - namespace linear_map /-- `T` is (semi-definite) **positive** if `T` is symmetric @@ -99,9 +80,9 @@ lemma is_positive.inner_nonneg_right {T : E โ†’โ‚—[๐•œ] E} (hT : is_positive T) hT.2 x /-- a linear projection onto `U` along its complement `V` is positive if -and only if `U` and `V` are pairwise orthogonal -/ +and only if `U` and `V` are orthogonal -/ lemma linear_proj_is_positive_iff {U V : submodule ๐•œ E} (hUV : is_compl U V) : - (U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_positive โ†” U.pairwise_orthogonal V := + (U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_positive โ†” U โŸ‚ V := begin split, { intros h u v, From bce4f554defddc5f5b4032d8622f2e1fcb0536e5 Mon Sep 17 00:00:00 2001 From: themathqueen <2497250a@research.gla.ac.uk> Date: Sat, 8 Apr 2023 13:23:55 +0000 Subject: [PATCH 6/9] fixes --- .../inner_product_space/positive.lean | 88 ++++++++++--------- .../inner_product_space/symmetric.lean | 5 +- 2 files changed, 48 insertions(+), 45 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index c2c7e69c07334..bc71c1f207d54 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -44,7 +44,11 @@ Positive operator -/ open inner_product_space is_R_or_C open_locale inner_product complex_conjugate -variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] + +variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] + [normed_add_comm_group E] [normed_add_comm_group F] + [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] + local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y namespace linear_map @@ -85,18 +89,24 @@ lemma linear_proj_is_positive_iff {U V : submodule ๐•œ E} (hUV : is_compl U V) (U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_positive โ†” U โŸ‚ V := begin split, - { intros h u v, - rw [โ† submodule.linear_proj_of_is_compl_apply_left hUV u, - โ† submodule.subtype_apply _, โ† comp_apply, h.1 _ _, - comp_apply, submodule.linear_proj_of_is_compl_apply_right hUV v, - map_zero, inner_zero_right], }, + { intros h u hu v hv, + let a : U := โŸจu, huโŸฉ, + let b : V := โŸจv, hvโŸฉ, + have hau : u = a := rfl, + have hbv : v = b := rfl, + rw [hau, โ† submodule.linear_proj_of_is_compl_apply_left hUV a, + โ† submodule.subtype_apply _, โ† comp_apply, โ† h.1 _ _, + comp_apply, hbv, submodule.linear_proj_of_is_compl_apply_right hUV b, + map_zero, inner_zero_left], }, { intro h, have : (U.subtype.comp (U.linear_proj_of_is_compl V hUV)).is_symmetric, { intros x y, nth_rewrite 0 โ† submodule.linear_proj_add_linear_proj_of_is_compl_eq_self hUV y, nth_rewrite 1 โ† submodule.linear_proj_add_linear_proj_of_is_compl_eq_self hUV x, simp_rw [inner_add_right, inner_add_left, comp_apply, - submodule.subtype_apply _, h _ _, inner_eq_zero_sym.mp (h _ _)], }, + submodule.subtype_apply _, โ† submodule.coe_inner, + submodule.is_ortho_iff_inner_eq.mp h _ (submodule.coe_mem _) _ (submodule.coe_mem _), + submodule.is_ortho_iff_inner_eq.mp h.symm _ (submodule.coe_mem _) _ (submodule.coe_mem _)], }, refine โŸจthis, _โŸฉ, intros x, rw [comp_apply, submodule.subtype_apply, @@ -150,9 +160,9 @@ begin calc T v = โˆ‘ i, โŸชe hT hn i, vโŸซ โ€ข T (e hT hn i) : _ ... = โˆ‘ i, ((โˆš (ฮฑ hT hn i) โ€ข โˆš (ฮฑ hT hn i)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข (e hT hn i) : _, simp_rw [โ† orthonormal_basis.repr_apply_apply, โ† map_smul_of_tower, โ† linear_map.map_sum, - orthonormal_basis.sum_repr (e hT hn) v, is_symmetric.apply_eigenvector_basis, - smul_smul, of_real_smul, โ† of_real_mul, โ† real.sqrt_mul (this _), - real.sqrt_mul_self (this _), mul_comm], + orthonormal_basis.sum_repr (e hT hn) v, is_symmetric.apply_eigenvector_basis, + smul_smul, of_real_smul, โ† of_real_mul, โ† real.sqrt_mul (this _), + real.sqrt_mul_self (this _), mul_comm], end /-- given a symmetric linear map `T` and a real number `r`, @@ -162,7 +172,7 @@ noncomputable def re_pow [decidable_eq ๐•œ] (hn : finite_dimensional.finrank { to_fun := ฮป v, โˆ‘ i : fin n, ((((ฮฑ hT hn i : โ„) ^ r : โ„)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i, map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, - ring_hom.id_apply, smul_smul, โ† mul_assoc, mul_comm] } + ring_hom.id_apply, smul_smul, โ† mul_assoc, mul_comm] } lemma re_pow_apply [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (r : โ„) (v : E) : @@ -190,13 +200,13 @@ lemma sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum (hT1 : (spectrum ๐•œ T).is_nonneg) : (T.sqrt hn hT) ^ 2 = T := by simp_rw [pow_two, mul_eq_comp, linear_map.ext_iff, comp_apply, sqrt_apply, - inner_sum, inner_smul_real_right, smul_smul, inner_smul_right, - โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, - euclidean_space.single_apply, mul_boole, smul_ite, smul_zero, - finset.sum_ite_eq, finset.mem_univ, if_true, algebra.mul_smul_comm, - sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1, - orthonormal_basis.repr_apply_apply, โ† smul_eq_mul, โ† smul_assoc, - eq_self_iff_true, forall_const] + inner_sum, inner_smul_real_right, smul_smul, inner_smul_right, + โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, + euclidean_space.single_apply, mul_boole, smul_ite, smul_zero, + finset.sum_ite_eq, finset.mem_univ, if_true, algebra.mul_smul_comm, + sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1, + orthonormal_basis.repr_apply_apply, โ† smul_eq_mul, โ† smul_assoc, + eq_self_iff_true, forall_const] /-- given a symmetric linear map `T`, we have that its root is positive -/ lemma is_symmetric.sqrt_is_positive @@ -206,18 +216,18 @@ begin have : (T.sqrt hn hT).is_symmetric, { intros x y, simp_rw [sqrt_apply T hn hT, inner_sum, sum_inner, smul_smul, inner_smul_right, - inner_smul_left], + inner_smul_left], have : โˆ€ i : fin n, conj ((โˆš (ฮฑ hT hn i)) : ๐•œ) = ((โˆš (ฮฑ hT hn i)) : ๐•œ) := ฮป i, by simp_rw [eq_conj_iff_re, of_real_re], - simp_rw [mul_assoc, map_mul, this _, inner_conj_sym, - mul_comm โŸชe hT hn _, yโŸซ _, โ† mul_assoc], }, + simp_rw [mul_assoc, map_mul, this, inner_conj_symm, + mul_comm โŸชe hT hn _, yโŸซ, โ† mul_assoc], }, refine โŸจthis, _โŸฉ, intro x, simp_rw [sqrt_apply _ hn hT, inner_sum, add_monoid_hom.map_sum, inner_smul_right], apply finset.sum_nonneg', intros i, - simp_rw [โ† inner_conj_sym x _, โ† orthonormal_basis.repr_apply_apply, - mul_conj, โ† of_real_mul, of_real_re], + simp_rw [โ† inner_conj_symm x, โ† orthonormal_basis.repr_apply_apply, + mul_conj, โ† of_real_mul, of_real_re], exact mul_nonneg (real.sqrt_nonneg _) (norm_sq_nonneg _), end @@ -233,9 +243,8 @@ begin ฮป h, โŸจh.1, _โŸฉโŸฉ, intros x, rw [โ† sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn h.1 h.2, - pow_two, mul_apply, โ† adjoint_inner_left, - is_self_adjoint_iff'.mp - ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn h.1).1)], + pow_two, mul_apply, โ† adjoint_inner_left, is_self_adjoint_iff'.mp + ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn h.1).1)], exact inner_self_nonneg, end @@ -252,7 +261,7 @@ begin use T.sqrt hn hT, rw [is_self_adjoint_iff'.mp ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn hT).1), - โ† pow_two], + โ† pow_two], exact (sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1).symm, }, { intros h, rcases h with โŸจS, rflโŸฉ, @@ -266,10 +275,11 @@ section complex /-- for spaces `V` over `โ„‚`, it suffices to define positivity with `0 โ‰ค โŸชv, T vโŸซ_โ„‚` for all `v โˆˆ V` -/ -lemma complex_is_positive {V : Type*} [inner_product_space โ„‚ V] (T : V โ†’โ‚—[โ„‚] V) : +lemma complex_is_positive {V : Type*} [normed_add_comm_group V] + [inner_product_space โ„‚ V] (T : V โ†’โ‚—[โ„‚] V) : T.is_positive โ†” โˆ€ v : V, โ†‘(re โŸชv, T vโŸซ_โ„‚) = โŸชv, T vโŸซ_โ„‚ โˆง 0 โ‰ค re โŸชv, T vโŸซ_โ„‚ := -by simp_rw [is_positive, is_symmetric_iff_inner_map_self_real, inner_conj_sym, - โ† eq_conj_iff_re, inner_conj_sym, โ† forall_and_distrib, and_comm, eq_comm] +by simp_rw [is_positive, is_symmetric_iff_inner_map_self_real, inner_conj_symm, + โ† eq_conj_iff_re, inner_conj_symm, โ† forall_and_distrib, and_comm, eq_comm] end complex @@ -279,7 +289,7 @@ lemma is_positive.conj_adjoint [finite_dimensional ๐•œ F] begin split, intros u v, - simp_rw [comp_apply, โ† adjoint_inner_left _ (T _), โ† adjoint_inner_right _ (T _) _], + simp_rw [comp_apply, โ† adjoint_inner_left _ (T _), โ† adjoint_inner_right _ (T _)], exact h.1 _ _, intros v, simp_rw [comp_apply, โ† adjoint_inner_left _ (T _)], @@ -311,11 +321,10 @@ is_symmetric.sqrt_is_positive _ hn (is_symmetric_adjoint_mul_self T) lemma norm_of_sqrt_adjoint_mul_self_eq [decidable_eq ๐•œ] (T : E โ†’โ‚—[๐•œ] E) (x : E) : โ€–(โˆšTโ‹†T) xโ€– = โ€–T xโ€– := begin -simp_rw [โ† sq_eq_sq (norm_nonneg _) (norm_nonneg _), - โ† inner_self_eq_norm_sq, โ† adjoint_inner_left, - is_self_adjoint_iff'.mp - ((is_symmetric_iff_is_self_adjoint _).mp (sqrt_adjoint_self_is_positive hn T).1), - โ† mul_eq_comp, โ† mul_apply, โ† pow_two, mul_eq_comp], + simp_rw [โ† sq_eq_sq (norm_nonneg _) (norm_nonneg _), โ† @inner_self_eq_norm_sq ๐•œ, + โ† adjoint_inner_left, is_self_adjoint_iff'.mp + ((is_symmetric_iff_is_self_adjoint _).mp (sqrt_adjoint_self_is_positive hn T).1), + โ† mul_eq_comp, โ† mul_apply, โ† pow_two, mul_eq_comp], congr, apply sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum, apply is_positive.nonneg_spectrum _ โŸจis_symmetric_adjoint_mul_self T, _โŸฉ, @@ -333,11 +342,7 @@ namespace continuous_linear_map open continuous_linear_map -variables {๐•œ E F : Type*} [is_R_or_C ๐•œ] -variables [normed_add_comm_group E] [normed_add_comm_group F] -variables [inner_product_space ๐•œ E] [inner_product_space ๐•œ F] variables [complete_space E] [complete_space F] -local notation `โŸช`x`, `y`โŸซ` := @inner ๐•œ _ _ x y /-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is self adjoint and `โˆ€ x, 0 โ‰ค re โŸชT x, xโŸซ`. -/ @@ -347,8 +352,7 @@ def is_positive (T : E โ†’L[๐•œ] E) : Prop := lemma is_positive.to_linear_map (T : E โ†’L[๐•œ] E) : T.to_linear_map.is_positive โ†” T.is_positive := by simp_rw [to_linear_map_eq_coe, linear_map.is_positive, continuous_linear_map.coe_coe, - is_positive, is_self_adjoint_iff_is_symmetric, re_apply_inner_self_apply T, - inner_re_symm] + is_positive, is_self_adjoint_iff_is_symmetric, re_apply_inner_self_apply T, inner_re_symm] lemma is_positive.is_self_adjoint {T : E โ†’L[๐•œ] E} (hT : is_positive T) : is_self_adjoint T := diff --git a/src/analysis/inner_product_space/symmetric.lean b/src/analysis/inner_product_space/symmetric.lean index bbef1843a52c7..0e6d9b2a6d545 100644 --- a/src/analysis/inner_product_space/symmetric.lean +++ b/src/analysis/inner_product_space/symmetric.lean @@ -155,9 +155,8 @@ end lemma is_symmetric_iff_real_inner (T : V โ†’โ‚—[โ„‚] V) : is_symmetric T โ†” โˆ€ x, (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ := begin - simp_rw [is_symmetric_iff_inner_map_self_real, - inner_conj_sym, โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re, - inner_conj_sym], + simp_rw [is_symmetric_iff_inner_map_self_real, inner_conj_symm, + โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re, inner_conj_symm], exact โŸจฮป h x, (h x).symm, ฮป h x, (h x).symmโŸฉ, end From e8b14bdebc24a2779939f1c5bb1e1945a70f6690 Mon Sep 17 00:00:00 2001 From: themathqueen <2497250a@research.gla.ac.uk> Date: Sun, 9 Apr 2023 09:45:12 +0000 Subject: [PATCH 7/9] change name and remove lemma --- .../inner_product_space/positive.lean | 23 +++++++++---------- .../inner_product_space/symmetric.lean | 8 ------- 2 files changed, 11 insertions(+), 20 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index bc71c1f207d54..69beef6ce251c 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -103,16 +103,15 @@ begin { intros x y, nth_rewrite 0 โ† submodule.linear_proj_add_linear_proj_of_is_compl_eq_self hUV y, nth_rewrite 1 โ† submodule.linear_proj_add_linear_proj_of_is_compl_eq_self hUV x, - simp_rw [inner_add_right, inner_add_left, comp_apply, - submodule.subtype_apply _, โ† submodule.coe_inner, - submodule.is_ortho_iff_inner_eq.mp h _ (submodule.coe_mem _) _ (submodule.coe_mem _), - submodule.is_ortho_iff_inner_eq.mp h.symm _ (submodule.coe_mem _) _ (submodule.coe_mem _)], }, + simp_rw [inner_add_right, inner_add_left, comp_apply, submodule.subtype_apply _, + โ† submodule.coe_inner, submodule.is_ortho_iff_inner_eq.mp h _ + (submodule.coe_mem _) _ (submodule.coe_mem _), + submodule.is_ortho_iff_inner_eq.mp h.symm _ + (submodule.coe_mem _) _ (submodule.coe_mem _)], }, refine โŸจthis, _โŸฉ, intros x, - rw [comp_apply, submodule.subtype_apply, - โ† submodule.linear_proj_of_is_compl_idempotent, - โ† submodule.subtype_apply, โ† comp_apply, - โ† this _ ((U.linear_proj_of_is_compl V hUV) x)], + rw [comp_apply, submodule.subtype_apply, โ† submodule.linear_proj_of_is_compl_idempotent, + โ† submodule.subtype_apply, โ† comp_apply, โ† this _ ((U.linear_proj_of_is_compl V hUV) x)], exact inner_self_nonneg, }, end @@ -167,22 +166,22 @@ end /-- given a symmetric linear map `T` and a real number `r`, we can define a linear map `S` such that `S = T ^ r` -/ -noncomputable def re_pow [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) +noncomputable def rpow [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (r : โ„) : E โ†’โ‚—[๐•œ] E := { to_fun := ฮป v, โˆ‘ i : fin n, ((((ฮฑ hT hn i : โ„) ^ r : โ„)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i, map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, ring_hom.id_apply, smul_smul, โ† mul_assoc, mul_comm] } -lemma re_pow_apply [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) +lemma rpow_apply [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) (r : โ„) (v : E) : - T.re_pow hn hT r v = โˆ‘ i : fin n, (((ฮฑ hT hn i : โ„) ^ r : โ„) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := + T.rpow hn hT r v = โˆ‘ i : fin n, (((ฮฑ hT hn i : โ„) ^ r : โ„) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := rfl /-- the square root of a symmetric linear map can then directly be defined with `re_pow` -/ noncomputable def sqrt [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (h : T.is_symmetric) : - E โ†’โ‚—[๐•œ] E := T.re_pow hn h (1 / 2 : โ„) + E โ†’โ‚—[๐•œ] E := T.rpow hn h (1 / 2 : โ„) /-- 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`, diff --git a/src/analysis/inner_product_space/symmetric.lean b/src/analysis/inner_product_space/symmetric.lean index 0e6d9b2a6d545..bd358edccdbbb 100644 --- a/src/analysis/inner_product_space/symmetric.lean +++ b/src/analysis/inner_product_space/symmetric.lean @@ -152,14 +152,6 @@ begin ring }, end -lemma is_symmetric_iff_real_inner (T : V โ†’โ‚—[โ„‚] V) : - is_symmetric T โ†” โˆ€ x, (โŸชx, T xโŸซ_โ„‚.re : โ„‚) = โŸชx, T xโŸซ_โ„‚ := -begin - simp_rw [is_symmetric_iff_inner_map_self_real, inner_conj_symm, - โ† is_R_or_C.re_eq_complex_re, โ† is_R_or_C.eq_conj_iff_re, inner_conj_symm], - exact โŸจฮป h x, (h x).symm, ฮป h x, (h x).symmโŸฉ, -end - end complex end linear_map From ee544c3fac1fb368a5e85f3a325b8c1827708ac9 Mon Sep 17 00:00:00 2001 From: themathqueen <2497250a@research.gla.ac.uk> Date: Sun, 9 Apr 2023 13:03:42 +0000 Subject: [PATCH 8/9] move results to new pr --- .../inner_product_space/positive.lean | 178 ++---------------- 1 file changed, 12 insertions(+), 166 deletions(-) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index 69beef6ce251c..1342ca4ab49c0 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -119,16 +119,8 @@ end def set.is_nonneg (A : set ๐•œ) : Prop := โˆ€ x : ๐•œ, x โˆˆ A โ†’ โ†‘(re x) = x โˆง 0 โ‰ค re x -section finite_dimensional - -local notation `e` := is_symmetric.eigenvector_basis -local notation `ฮฑ` := is_symmetric.eigenvalues -local notation `โˆš` := real.sqrt - -variables {n : โ„•} [finite_dimensional ๐•œ E] (T : E โ†’โ‚—[๐•œ] E) - /-- the spectrum of a positive linear map is non-negative -/ -lemma is_positive.nonneg_spectrum (h : T.is_positive) : +lemma is_positive.nonneg_spectrum [finite_dimensional ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} (h : T.is_positive) : (spectrum ๐•œ T).is_nonneg := begin cases h with hT h, @@ -141,135 +133,6 @@ begin exact โŸจthis, eigenvalue_nonneg_of_nonneg hฮผ hโŸฉ, end -open_locale big_operators -/-- 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`) -/ -lemma sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum - [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) - (hT1 : (spectrum ๐•œ T).is_nonneg) (v : E) : - T v = โˆ‘ i, ((โˆš (ฮฑ hT hn i) โ€ข โˆš (ฮฑ hT hn i)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := -begin - have : โˆ€ i : fin n, 0 โ‰ค ฮฑ hT hn i := ฮป i, - by { specialize hT1 (hT.eigenvalues hn i), - simp only [of_real_re, eq_self_iff_true, true_and] at hT1, - apply hT1 (module.End.mem_spectrum_of_has_eigenvalue - (is_symmetric.has_eigenvalue_eigenvalues hT hn i)), }, - calc T v = โˆ‘ i, โŸชe hT hn i, vโŸซ โ€ข T (e hT hn i) : _ - ... = โˆ‘ i, ((โˆš (ฮฑ hT hn i) โ€ข โˆš (ฮฑ hT hn i)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข (e hT hn i) : _, - simp_rw [โ† orthonormal_basis.repr_apply_apply, โ† map_smul_of_tower, โ† linear_map.map_sum, - orthonormal_basis.sum_repr (e hT hn) v, is_symmetric.apply_eigenvector_basis, - smul_smul, of_real_smul, โ† of_real_mul, โ† real.sqrt_mul (this _), - real.sqrt_mul_self (this _), mul_comm], -end - -/-- given a symmetric linear map `T` and a real number `r`, -we can define a linear map `S` such that `S = T ^ r` -/ -noncomputable def rpow [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) - (hT : T.is_symmetric) (r : โ„) : E โ†’โ‚—[๐•œ] E := -{ to_fun := ฮป v, โˆ‘ i : fin n, ((((ฮฑ hT hn i : โ„) ^ r : โ„)) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i, - map_add' := ฮป x y, by simp_rw [inner_add_right, add_smul, smul_add, finset.sum_add_distrib], - map_smul' := ฮป r x, by simp_rw [inner_smul_right, โ† smul_smul, finset.smul_sum, - ring_hom.id_apply, smul_smul, โ† mul_assoc, mul_comm] } - -lemma rpow_apply [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) - (hT : T.is_symmetric) (r : โ„) (v : E) : - T.rpow hn hT r v = โˆ‘ i : fin n, (((ฮฑ hT hn i : โ„) ^ r : โ„) : ๐•œ) โ€ข โŸชe hT hn i, vโŸซ โ€ข e hT hn i := -rfl - -/-- the square root of a symmetric linear map can then directly be defined with `re_pow` -/ -noncomputable def sqrt [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) - (h : T.is_symmetric) : - E โ†’โ‚—[๐•œ] E := T.rpow hn h (1 / 2 : โ„) - -/-- 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`) -/ -lemma sqrt_apply (hn : finite_dimensional.finrank ๐•œ E = n) [decidable_eq ๐•œ] - (hT : T.is_symmetric) (x : E) : - T.sqrt hn hT x = โˆ‘ i, (โˆš (ฮฑ hT hn i) : ๐•œ) โ€ข โŸชe hT hn i, xโŸซ โ€ข e hT hn i := -by { simp_rw [real.sqrt_eq_rpow _], refl } - -/-- 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` -/ -lemma sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum - [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) - (hT1 : (spectrum ๐•œ T).is_nonneg) : - (T.sqrt hn hT) ^ 2 = T := -by simp_rw [pow_two, mul_eq_comp, linear_map.ext_iff, comp_apply, sqrt_apply, - inner_sum, inner_smul_real_right, smul_smul, inner_smul_right, - โ† orthonormal_basis.repr_apply_apply, orthonormal_basis.repr_self, - euclidean_space.single_apply, mul_boole, smul_ite, smul_zero, - finset.sum_ite_eq, finset.mem_univ, if_true, algebra.mul_smul_comm, - sq_mul_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1, - orthonormal_basis.repr_apply_apply, โ† smul_eq_mul, โ† smul_assoc, - eq_self_iff_true, forall_const] - -/-- given a symmetric linear map `T`, we have that its root is positive -/ -lemma is_symmetric.sqrt_is_positive - [decidable_eq ๐•œ] (hn : finite_dimensional.finrank ๐•œ E = n) (hT : T.is_symmetric) : - (T.sqrt hn hT).is_positive := -begin - have : (T.sqrt hn hT).is_symmetric, - { intros x y, - simp_rw [sqrt_apply T hn hT, inner_sum, sum_inner, smul_smul, inner_smul_right, - inner_smul_left], - have : โˆ€ i : fin n, conj ((โˆš (ฮฑ hT hn i)) : ๐•œ) = ((โˆš (ฮฑ hT hn i)) : ๐•œ) := ฮป i, - by simp_rw [eq_conj_iff_re, of_real_re], - simp_rw [mul_assoc, map_mul, this, inner_conj_symm, - mul_comm โŸชe hT hn _, yโŸซ, โ† mul_assoc], }, - refine โŸจthis, _โŸฉ, - intro x, - simp_rw [sqrt_apply _ hn hT, inner_sum, add_monoid_hom.map_sum, inner_smul_right], - apply finset.sum_nonneg', - intros i, - simp_rw [โ† inner_conj_symm x, โ† orthonormal_basis.repr_apply_apply, - mul_conj, โ† of_real_mul, of_real_re], - exact mul_nonneg (real.sqrt_nonneg _) (norm_sq_nonneg _), -end - -/-- `T` is positive if and only if `T` is symmetric -(which is automatic from the definition of positivity) -and has a non-negative spectrum -/ -lemma is_positive_iff_is_symmetric_and_nonneg_spectrum - (hn : finite_dimensional.finrank ๐•œ E = n) : - T.is_positive โ†” T.is_symmetric โˆง (spectrum ๐•œ T).is_nonneg := -begin - classical, - refine โŸจฮป h, โŸจh.1, ฮป ฮผ hฮผ, is_positive.nonneg_spectrum T h ฮผ hฮผโŸฉ, - ฮป h, โŸจh.1, _โŸฉโŸฉ, - intros x, - rw [โ† sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn h.1 h.2, - pow_two, mul_apply, โ† adjoint_inner_left, is_self_adjoint_iff'.mp - ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn h.1).1)], - exact inner_self_nonneg, -end - -/-- `T` is positive if and only if there exists a -linear map `S` such that `T = S.adjoint * S` -/ -lemma is_positive_iff_exists_adjoint_mul_self - (hn : finite_dimensional.finrank ๐•œ E = n) : - T.is_positive โ†” โˆƒ S : E โ†’โ‚—[๐•œ] E, T = S.adjoint * S := -begin - classical, - split, - { rw [is_positive_iff_is_symmetric_and_nonneg_spectrum T hn], - rintro โŸจhT, hT1โŸฉ, - use T.sqrt hn hT, - rw [is_self_adjoint_iff'.mp - ((is_symmetric_iff_is_self_adjoint _).mp (is_symmetric.sqrt_is_positive T hn hT).1), - โ† pow_two], - exact (sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum T hn hT hT1).symm, }, - { intros h, - rcases h with โŸจS, rflโŸฉ, - refine โŸจis_symmetric_adjoint_mul_self S, _โŸฉ, - intro x, - simp_rw [mul_apply, adjoint_inner_right], - exact inner_self_nonneg, }, -end - section complex /-- for spaces `V` over `โ„‚`, it suffices to define positivity with @@ -282,7 +145,7 @@ by simp_rw [is_positive, is_symmetric_iff_inner_map_self_real, inner_conj_symm, end complex -lemma is_positive.conj_adjoint [finite_dimensional ๐•œ F] +lemma is_positive.conj_adjoint [finite_dimensional ๐•œ E] [finite_dimensional ๐•œ F] (T : E โ†’โ‚—[๐•œ] E) (S : E โ†’โ‚—[๐•œ] F) (h : T.is_positive) : (S.comp (T.comp S.adjoint)).is_positive := begin @@ -295,7 +158,7 @@ begin exact h.2 _, end -lemma is_positive.adjoint_conj [finite_dimensional ๐•œ F] +lemma is_positive.adjoint_conj [finite_dimensional ๐•œ E] [finite_dimensional ๐•œ F] (T : E โ†’โ‚—[๐•œ] E) (S : F โ†’โ‚—[๐•œ] E) (h : T.is_positive) : (S.adjoint.comp (T.comp S)).is_positive := begin @@ -308,32 +171,6 @@ begin exact h.2 _, end -variable (hn : finite_dimensional.finrank ๐•œ E = n) -local notation `โˆšTโ‹†`T := (T.adjoint.comp T).sqrt hn (is_symmetric_adjoint_mul_self T) - -/-- we have `(T.adjoint.comp T).sqrt` is positive, given any linear map `T` -/ -lemma sqrt_adjoint_self_is_positive [decidable_eq ๐•œ] (T : E โ†’โ‚—[๐•œ] E) : (โˆšTโ‹†T).is_positive := -is_symmetric.sqrt_is_positive _ hn (is_symmetric_adjoint_mul_self T) - -/-- given any linear map `T` and `x โˆˆ E` we have -`โ€–(T.adjoint.comp T).sqrt xโ€– = โ€–T xโ€–` -/ -lemma norm_of_sqrt_adjoint_mul_self_eq [decidable_eq ๐•œ] (T : E โ†’โ‚—[๐•œ] E) (x : E) : - โ€–(โˆšTโ‹†T) xโ€– = โ€–T xโ€– := -begin - simp_rw [โ† sq_eq_sq (norm_nonneg _) (norm_nonneg _), โ† @inner_self_eq_norm_sq ๐•œ, - โ† adjoint_inner_left, is_self_adjoint_iff'.mp - ((is_symmetric_iff_is_self_adjoint _).mp (sqrt_adjoint_self_is_positive hn T).1), - โ† mul_eq_comp, โ† mul_apply, โ† pow_two, mul_eq_comp], - congr, - apply sqrt_sq_eq_self_of_is_symmetric_and_nonneg_spectrum, - apply is_positive.nonneg_spectrum _ โŸจis_symmetric_adjoint_mul_self T, _โŸฉ, - intros x, - simp_rw [mul_apply, adjoint_inner_right], - exact inner_self_nonneg, -end - -end finite_dimensional - end linear_map @@ -430,3 +267,12 @@ end end complex end continuous_linear_map + +lemma orthogonal_projection_is_positive [complete_space E] (U : submodule ๐•œ E) [complete_space U] : + (U.subtypeL โˆ˜L (orthogonal_projection U)).is_positive := +begin + refine โŸจorthogonal_projection_is_self_adjoint U, ฮป x, _โŸฉ, + simp_rw [continuous_linear_map.re_apply_inner_self, โ† submodule.adjoint_orthogonal_projection, + continuous_linear_map.comp_apply, continuous_linear_map.adjoint_inner_left], + exact inner_self_nonneg, +end From 8b9324da618b7c46d51e48deeb182fe4f56decd5 Mon Sep 17 00:00:00 2001 From: themathqueen <2497250a@research.gla.ac.uk> Date: Mon, 10 Apr 2023 09:43:36 +0000 Subject: [PATCH 9/9] feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive --- .../inner_product_space/positive.lean | 17 ++++++++++ src/linear_algebra/matrix/pos_def.lean | 33 +++++++++++++++++++ 2 files changed, 50 insertions(+) diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean index 1342ca4ab49c0..264abeb7c914b 100644 --- a/src/analysis/inner_product_space/positive.lean +++ b/src/analysis/inner_product_space/positive.lean @@ -5,6 +5,7 @@ Authors: Anatole Dedecker -/ import analysis.inner_product_space.adjoint import analysis.inner_product_space.spectrum +import linear_algebra.matrix.pos_def /-! # Positive operators @@ -276,3 +277,19 @@ begin continuous_linear_map.comp_apply, continuous_linear_map.adjoint_inner_left], exact inner_self_nonneg, end + +lemma matrix.pos_semidef_eq_linear_map_positive + {n : Type*} [fintype n] [decidable_eq n] (x : matrix n n ๐•œ) : + (x.pos_semidef) โ†” x.to_euclidean_lin.is_positive := +begin + have : x.to_euclidean_lin = ((pi_Lp.linear_equiv 2 ๐•œ (ฮป _ : n, ๐•œ)).symm.conj + x.to_lin' : module.End ๐•œ (pi_Lp 2 _)) := rfl, + simp_rw [linear_map.is_positive, โ† matrix.is_hermitian_iff_is_symmetric, matrix.pos_semidef, + this, pi_Lp.inner_apply, is_R_or_C.inner_apply, map_sum, linear_equiv.conj_apply, + linear_map.comp_apply, linear_equiv.coe_coe, pi_Lp.linear_equiv_symm_apply, + linear_equiv.symm_symm, pi_Lp.linear_equiv_apply, matrix.to_lin'_apply, + pi_Lp.equiv_symm_apply, โ† is_R_or_C.star_def, matrix.mul_vec, matrix.dot_product, + pi_Lp.equiv_apply, โ† pi.mul_apply (x _) _, โ† matrix.dot_product, map_sum, pi.star_apply, + matrix.mul_vec, matrix.dot_product, pi.mul_apply], + refl, +end diff --git a/src/linear_algebra/matrix/pos_def.lean b/src/linear_algebra/matrix/pos_def.lean index c814a4996c235..47a63bded5cdb 100644 --- a/src/linear_algebra/matrix/pos_def.lean +++ b/src/linear_algebra/matrix/pos_def.lean @@ -34,6 +34,39 @@ lemma pos_def.is_hermitian {M : matrix n n ๐•œ} (hM : M.pos_def) : M.is_hermiti def pos_semidef (M : matrix n n ๐•œ) := M.is_hermitian โˆง โˆ€ x : n โ†’ ๐•œ, 0 โ‰ค is_R_or_C.re (dot_product (star x) (M.mul_vec x)) +lemma pos_semidef.conj_transpose_mul_self (x : matrix n n ๐•œ) : + (x.conj_transpose.mul x).pos_semidef := +begin + refine โŸจis_hermitian_transpose_mul_self _, ฮป y, _โŸฉ, + have : is_R_or_C.re (dot_product (star y) ((x.conj_transpose.mul x).mul_vec y)) + = is_R_or_C.re (dot_product (star (x.mul_vec y)) (x.mul_vec y)), + { simp only [star_mul_vec, dot_product_mul_vec, + vec_mul_vec_mul], }, + rw [this], + clear this, + simp_rw [dot_product, map_sum], + apply finset.sum_nonneg', + intros i, + simp_rw [pi.star_apply, is_R_or_C.star_def, โ† is_R_or_C.inner_apply], + exact inner_self_nonneg, +end + +lemma pos_semidef.conj_transpose {x : matrix n n ๐•œ} (hx : x.pos_semidef) : + x.conj_transpose.pos_semidef := +begin + refine โŸจis_hermitian.conj_transpose hx.1, ฮป y, _โŸฉ, + rw [star_dot_product, star_mul_vec, conj_transpose_conj_transpose, + โ† dot_product_mul_vec, is_R_or_C.star_def, is_R_or_C.conj_re], + exact hx.2 _, +end + +lemma pos_semidef.self_mul_conj_transpose (x : matrix n n ๐•œ) : + (x.mul x.conj_transpose).pos_semidef := +begin + nth_rewrite 0 โ† conj_transpose_conj_transpose x, + exact pos_semidef.conj_transpose_mul_self _, +end + lemma pos_def.pos_semidef {M : matrix n n ๐•œ} (hM : M.pos_def) : M.pos_semidef := begin refine โŸจhM.1, _โŸฉ,