feat(analysis/inner_product_space/positive): definition and basic fac…

…ts about positive operators (#15470)

src/analysis/inner_product_space/adjoint.lean

@@ -77,6 +77,26 @@ by rw [hT x y, inner_conj_sym]
   ⟪T x, y⟫ = ⟪x, T y⟫ :=
 hT x y
 
+lemma is_self_adjoint_zero : is_self_adjoint (0 : E →ₗ[𝕜] E) :=
+λ x y, (inner_zero_right : ⟪x, 0⟫ = 0).symm ▸ (inner_zero_left : ⟪0, y⟫ = 0)
+
+lemma is_self_adjoint_id : is_self_adjoint (linear_map.id : E →ₗ[𝕜] E) :=
+λ x y, rfl
+
+lemma is_self_adjoint.add {T S : E →ₗ[𝕜] E} (hT : is_self_adjoint T)
+  (hS : is_self_adjoint S) : is_self_adjoint (T + S) :=
+begin
+  intros x y,
+  rw [linear_map.add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right],
+  refl
+end
+
+/-- The orthogonal projection is self-adjoint. -/
+lemma orthogonal_projection_is_self_adjoint [complete_space E] (U : submodule 𝕜 E)
+  [complete_space U] :
+  is_self_adjoint (U.subtypeL ∘L orthogonal_projection U : E →ₗ[𝕜] E):=
+inner_orthogonal_projection_left_eq_right U
+
 /-- The **Hellinger--Toeplitz theorem**: if a symmetric operator is defined everywhere, then
   it is automatically continuous. -/
 lemma is_self_adjoint.continuous [complete_space E] {T : E →ₗ[𝕜] E} (hT : is_self_adjoint T) :
@@ -254,6 +274,58 @@ begin
   exact ext_inner_right 𝕜 (λ y, by simp only [adjoint_inner_left, h x y])
 end
 
+@[simp] lemma is_self_adjoint_iff_adjoint_eq (A : E →L[𝕜] E) :
+  is_self_adjoint (A : E →ₗ[𝕜] E) ↔ A† = A :=
+by simp_rw [is_self_adjoint, coe_coe, ← eq_adjoint_iff, eq_comm]
+
+lemma _root_.inner_product_space.is_self_adjoint.adjoint_eq {A : E →L[𝕜] E}
+  (hA : is_self_adjoint (A : E →ₗ[𝕜] E)) : A† = A :=
+by rwa is_self_adjoint_iff_adjoint_eq at hA
+
+lemma _root_.inner_product_space.is_self_adjoint.conj_adjoint {T : E →L[𝕜] E}
+  (hT : is_self_adjoint (T : E →ₗ[𝕜] E)) (S : E →L[𝕜] F) :
+  is_self_adjoint (S ∘L T ∘L S† : F →ₗ[𝕜] F) :=
+begin
+  intros x y,
+  rw [coe_coe, comp_apply, comp_apply, ← adjoint_inner_right, ← coe_coe, hT, coe_coe,
+      adjoint_inner_left],
+  refl
+end
+
+lemma _root_.inner_product_space.is_self_adjoint.adjoint_conj {T : E →L[𝕜] E}
+  (hT : is_self_adjoint (T : E →ₗ[𝕜] E)) (S : F →L[𝕜] E) :
+  is_self_adjoint (S† ∘L T ∘L S : F →ₗ[𝕜] F) :=
+begin
+  convert hT.conj_adjoint (S†),
+  rw adjoint_adjoint
+end
+
+lemma _root_.inner_product_space.is_self_adjoint.conj_orthogonal_projection {T : E →L[𝕜] E}
+  (hT : is_self_adjoint (T : E →ₗ[𝕜] E)) (U : submodule 𝕜 E) [complete_space U] :
+  is_self_adjoint (U.subtypeL ∘L orthogonal_projection U ∘L T ∘L U.subtypeL ∘L
+    orthogonal_projection U : E →ₗ[𝕜] E) :=
+begin
+  have := hT.conj_adjoint (U.subtypeL ∘L orthogonal_projection U),
+  rwa (orthogonal_projection_is_self_adjoint U).adjoint_eq at this
+end
+
+lemma _root_.submodule.adjoint_subtypeL (U : submodule 𝕜 E)
+  [complete_space U] :
+  (U.subtypeL)† = orthogonal_projection U :=
+begin
+  symmetry,
+  rw eq_adjoint_iff,
+  intros x u,
+  rw [U.coe_inner, inner_orthogonal_projection_left_eq_right,
+      orthogonal_projection_mem_subspace_eq_self],
+  refl
+end
+
+lemma _root_.submodule.adjoint_orthogonal_projection (U : submodule 𝕜 E)
+  [complete_space U] :
+  (orthogonal_projection U : E →L[𝕜] U)† = U.subtypeL :=
+by rw [← U.adjoint_subtypeL, adjoint_adjoint]
+
 /-- `E →L[𝕜] E` is a star algebra with the adjoint as the star operation. -/
 instance : has_star (E →L[𝕜] E) := ⟨adjoint⟩
 instance : has_involutive_star (E →L[𝕜] E) := ⟨adjoint_adjoint⟩

src/analysis/inner_product_space/positive.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2022 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+import analysis.inner_product_space.l2_space
+import analysis.inner_product_space.adjoint
+
+/-!
+# Positive operators
+
+In this file we define positive operators in a Hilbert space. We follow Bourbaki's choice
+of requiring self adjointness in the definition.
+
+## Main definitions
+
+* `is_positive` : a continuous linear map is positive if it is self adjoint and
+  `∀ x, 0 ≤ re ⟪T x, x⟫`
+
+## Main statements
+
+* `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,
+  checking that `⟪T x, x⟫` is a nonnegative real number for all `x` suffices to prove that
+  `T` is positive
+
+## References
+
+* [Bourbaki, *Topological Vector Spaces*][bourbaki1987]
+
+## Tags
+
+Positive operator
+-/
+
+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]
+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⟫`. -/
+def is_positive (T : E →L[𝕜] E) : Prop :=
+  is_self_adjoint (T : E →ₗ[𝕜] E) ∧ ∀ x, 0 ≤ T.re_apply_inner_self x
+
+lemma is_positive.is_self_adjoint {T : E →L[𝕜] E} (hT : is_positive T) :
+  is_self_adjoint (T : E →ₗ[𝕜] E) :=
+hT.1
+
+lemma is_positive.inner_nonneg_left {T : E →L[𝕜] E} (hT : is_positive T) (x : E) :
+  0 ≤ re ⟪T x, x⟫ :=
+hT.2 x
+
+lemma is_positive.inner_nonneg_right {T : E →L[𝕜] E} (hT : is_positive T) (x : E) :
+  0 ≤ re ⟪x, T x⟫ :=
+by rw inner_re_symm; exact hT.inner_nonneg_left x
+
+lemma is_positive_zero : is_positive (0 : E →L[𝕜] E) :=
+begin
+  refine ⟨is_self_adjoint_zero, λ x, _⟩,
+  change 0 ≤ re ⟪_, _⟫,
+  rw [zero_apply, inner_zero_left, zero_hom_class.map_zero]
+end
+
+lemma is_positive_id : is_positive (1 : E →L[𝕜] E) :=
+⟨λ x y, rfl, λ x, inner_self_nonneg⟩
+
+lemma is_positive.add {T S : E →L[𝕜] E} (hT : T.is_positive)
+  (hS : S.is_positive) : (T + S).is_positive :=
+begin
+  refine ⟨hT.is_self_adjoint.add hS.is_self_adjoint, λ x, _⟩,
+  rw [re_apply_inner_self, add_apply, inner_add_left, map_add],
+  exact add_nonneg (hT.inner_nonneg_left x) (hS.inner_nonneg_left x)
+end
+
+lemma is_positive.conj_adjoint [complete_space E] [complete_space F] {T : E →L[𝕜] E}
+  (hT : T.is_positive) (S : E →L[𝕜] F) : (S ∘L T ∘L S†).is_positive :=
+begin
+  refine ⟨hT.is_self_adjoint.conj_adjoint S, λ x, _⟩,
+  rw [re_apply_inner_self, comp_apply, ← adjoint_inner_right],
+  exact hT.inner_nonneg_left _
+end
+
+lemma is_positive.adjoint_conj [complete_space E] [complete_space F] {T : E →L[𝕜] E}
+  (hT : T.is_positive) (S : F →L[𝕜] E) : (S† ∘L T ∘L S).is_positive :=
+begin
+  convert hT.conj_adjoint (S†),
+  rw adjoint_adjoint
+end
+
+lemma is_positive.conj_orthogonal_projection [complete_space E] (U : submodule 𝕜 E) {T : E →L[𝕜] E}
+  (hT : T.is_positive) [complete_space U] :
+  (U.subtypeL ∘L orthogonal_projection U ∘L T ∘L U.subtypeL ∘L
+    orthogonal_projection U).is_positive :=
+begin
+  have := hT.conj_adjoint (U.subtypeL ∘L orthogonal_projection U),
+  rwa (orthogonal_projection_is_self_adjoint U).adjoint_eq at this
+end
+
+lemma is_positive.orthogonal_projection_comp [complete_space E] {T : E →L[𝕜] E}
+  (hT : T.is_positive) (U : submodule 𝕜 E) [complete_space U] :
+  (orthogonal_projection U ∘L T ∘L U.subtypeL).is_positive :=
+begin
+  have := hT.conj_adjoint (orthogonal_projection U : E →L[𝕜] U),
+  rwa [U.adjoint_orthogonal_projection] at this,
+end
+
+section complex
+
+variables {E' : Type*} [inner_product_space ℂ E']
+
+lemma is_positive_iff_complex (T : E' →L[ℂ] E') :
+  is_positive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ :=
+begin
+  simp_rw [is_positive, forall_and_distrib, is_self_adjoint_iff_inner_map_self_real,
+    eq_conj_iff_re],
+  refl
+end
+
+end complex
+
+end continuous_linear_map