feat: define IsPositive and Löwner order for LinearMap (leanprover-community#24471)

Moves:
- ContinuousLinearMap.IsPositive.inner_nonneg_left -> ContinuousLinearMap.IsPositive.re_inner_nonneg_left
- ContinuousLinearMap.IsPositive.inner_nonneg_right -> ContinuousLinearMap.IsPositive.re_inner_nonneg_right

Author: IvanRenison

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -451,6 +451,20 @@ theorem im_inner_adjoint_mul_self_eq_zero (T : E →ₗ[𝕜] E) (x : E) :
   simp only [Module.End.mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]
   norm_cast
 
+theorem isSelfAdjoint_toContinuousLinearMap_iff [CompleteSpace E] (T : E →ₗ[𝕜] E) :
+    IsSelfAdjoint T.toContinuousLinearMap ↔ IsSelfAdjoint T := by
+  simp only [IsSelfAdjoint, star, adjoint, LinearEquiv.trans_apply,
+      coe_toContinuousLinearMap_symm,
+      ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]
+  rfl
+
+theorem _root_.ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff [CompleteSpace E] (T : E →L[𝕜] E) :
+    IsSelfAdjoint T.toLinearMap ↔ IsSelfAdjoint T := by
+  simp only [IsSelfAdjoint, star, adjoint, LinearEquiv.trans_apply,
+      coe_toContinuousLinearMap_symm,
+      ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]
+  rfl
+
 end LinearMap
 
 section Unitary

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -8,21 +8,23 @@ import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 # Positive operators
 
-In this file we define positive operators in a Hilbert space. We follow Bourbaki's choice
+In this file we define when an operator in a Hilbert space is positive. We follow Bourbaki's choice
 of requiring self adjointness in the definition.
 
 ## Main definitions
 
-* `IsPositive` : a continuous linear map is positive if it is self adjoint and
-  `∀ x, 0 ≤ re ⟪T x, x⟫`
+* `LinearMap.IsPositive` : a linear map is positive if it is self adjoint and
+  `∀ x, 0 ≤ re ⟪T x, x⟫`.
+* `ContinuousLinearMap.IsPositive` : a continuous linear map is positive if it is self adjoint and
+  `∀ x, 0 ≤ re ⟪T x, x⟫`.
 
 ## Main statements
 
 * `ContinuousLinearMap.IsPositive.conj_adjoint` : if `T : E →L[𝕜] E` is positive,
   then for any `S : E →L[𝕜] F`, `S ∘L T ∘L S†` is also positive.
 * `ContinuousLinearMap.isPositive_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
+  `T` is positive.
 
 ## References
 
@@ -33,20 +35,20 @@ of requiring self adjointness in the definition.
 Positive operator
 -/
 
-
-open InnerProductSpace RCLike ContinuousLinearMap
+open InnerProductSpace RCLike LinearMap ContinuousLinearMap
 
 open scoped InnerProduct ComplexConjugate
 
-namespace ContinuousLinearMap
-
 variable {𝕜 E F : Type*} [RCLike 𝕜]
 variable [NormedAddCommGroup E] [NormedAddCommGroup F]
 variable [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F]
-variable [CompleteSpace E] [CompleteSpace F]
 
 local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
 
+namespace ContinuousLinearMap
+
+variable [CompleteSpace E] [CompleteSpace 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 IsPositive (T : E →L[𝕜] E) : Prop :=
@@ -55,33 +57,72 @@ def IsPositive (T : E →L[𝕜] E) : Prop :=
 theorem IsPositive.isSelfAdjoint {T : E →L[𝕜] E} (hT : IsPositive T) : IsSelfAdjoint T :=
   hT.1
 
-theorem IsPositive.inner_nonneg_left {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
+theorem IsPositive.inner_left_eq_inner_right {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
+    ⟪T x, x⟫ = ⟪x, T x⟫ := by
+  rw [← adjoint_inner_left, show adjoint T = T from hT.left]
+
+theorem IsPositive.re_inner_nonneg_left {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
     0 ≤ re ⟪T x, x⟫ :=
   hT.2 x
 
+theorem IsPositive.re_inner_nonneg_right {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
+    0 ≤ re ⟪x, T x⟫ := by rw [inner_re_symm]; exact hT.re_inner_nonneg_left x
+
+open ComplexOrder in
+theorem isPositive_iff (T : E →L[𝕜] E) :
+    IsPositive T ↔ IsSelfAdjoint T ∧ ∀ x, 0 ≤ ⟪T x, x⟫ := by
+  simp_rw [IsPositive, and_congr_right_iff, ← RCLike.ofReal_nonneg (K := 𝕜), reApplyInnerSelf_apply]
+  intro hT
+  have := hT.isSymmetric.coe_re_inner_apply_self
+  simp_all
+
+open ComplexOrder in
+theorem IsPositive.inner_nonneg_left {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
+    0 ≤ ⟪T x, x⟫ :=
+  ((isPositive_iff T).mp hT).right x
+
+open ComplexOrder in
 theorem IsPositive.inner_nonneg_right {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
-    0 ≤ re ⟪x, T x⟫ := by rw [inner_re_symm]; exact hT.inner_nonneg_left x
+    0 ≤ ⟪x, T x⟫ := by
+  rw [← hT.inner_left_eq_inner_right]
+  exact inner_nonneg_left hT x
 
+@[simp]
 theorem isPositive_zero : IsPositive (0 : E →L[𝕜] E) := by
   refine ⟨.zero _, fun x => ?_⟩
   change 0 ≤ re ⟪_, _⟫
   rw [zero_apply, inner_zero_left, ZeroHomClass.map_zero]
 
+@[simp]
 theorem isPositive_one : IsPositive (1 : E →L[𝕜] E) :=
   ⟨.one _, fun _ => inner_self_nonneg⟩
 
+@[simp]
+theorem isPositive_natCast {n : ℕ} : IsPositive (n : E →L[𝕜] E) := by
+  refine ⟨IsSelfAdjoint.natCast n, ?_⟩
+  intro x
+  simp [reApplyInnerSelf, ← Nat.cast_smul_eq_nsmul 𝕜, inner_smul_left]
+  exact mul_nonneg n.cast_nonneg' inner_self_nonneg
+
+@[simp]
+theorem isPositive_ofNat {n : ℕ} [n.AtLeastTwo] : IsPositive (ofNat(n) : E →L[𝕜] E) :=
+  isPositive_natCast
+
+@[aesop safe apply]
 theorem IsPositive.add {T S : E →L[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) :
     (T + S).IsPositive := by
   refine ⟨hT.isSelfAdjoint.add hS.isSelfAdjoint, fun x => ?_⟩
   rw [reApplyInnerSelf, add_apply, inner_add_left, map_add]
-  exact add_nonneg (hT.inner_nonneg_left x) (hS.inner_nonneg_left x)
+  exact add_nonneg (hT.re_inner_nonneg_left x) (hS.re_inner_nonneg_left x)
 
+@[aesop safe apply]
 theorem IsPositive.conj_adjoint {T : E →L[𝕜] E} (hT : T.IsPositive) (S : E →L[𝕜] F) :
     (S ∘L T ∘L S†).IsPositive := by
   refine ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩
   rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]
-  exact hT.inner_nonneg_left _
+  exact hT.re_inner_nonneg_left _
 
+@[aesop safe apply]
 theorem IsPositive.adjoint_conj {T : E →L[𝕜] E} (hT : T.IsPositive) (S : F →L[𝕜] E) :
     (S† ∘L T ∘L S).IsPositive := by
   convert hT.conj_adjoint (S†)
@@ -144,20 +185,16 @@ section PartialOrder
 `StarOrderedRing`. -/
 instance instLoewnerPartialOrder : PartialOrder (E →L[𝕜] E) where
   le f g := (g - f).IsPositive
-  le_refl _ := by simpa using isPositive_zero
+  le_refl _ := by simp
   le_trans _ _ _ h₁ h₂ := by simpa using h₁.add h₂
   le_antisymm f₁ f₂ h₁ h₂ := by
     rw [← sub_eq_zero]
     have h_isSymm := isSelfAdjoint_iff_isSymmetric.mp <| IsPositive.isSelfAdjoint h₂
     exact_mod_cast h_isSymm.inner_map_self_eq_zero.mp fun x ↦ by
-      apply RCLike.ext
-      · rw [map_zero]
-        apply le_antisymm
-        · rw [← neg_nonneg, ← map_neg, ← inner_neg_left]
-          simpa using h₁.inner_nonneg_left _
-        · exact h₂.inner_nonneg_left _
-      · rw [coe_sub, LinearMap.sub_apply, coe_coe, coe_coe, map_zero, ← sub_apply,
-          ← h_isSymm.coe_reApplyInnerSelf_apply (T := f₁ - f₂) x, RCLike.ofReal_im]
+      open scoped ComplexOrder in
+      refine le_antisymm ?_ (h₂.inner_nonneg_left x)
+      rw [← neg_nonneg, ← inner_neg_left]
+      simpa using h₁.inner_nonneg_left x
 
 lemma le_def (f g : E →L[𝕜] E) : f ≤ g ↔ (g - f).IsPositive := Iff.rfl
 
@@ -167,3 +204,155 @@ lemma nonneg_iff_isPositive (f : E →L[𝕜] E) : 0 ≤ f ↔ f.IsPositive := b
 end PartialOrder
 
 end ContinuousLinearMap
+
+namespace LinearMap
+
+variable [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F]
+
+/-- A linear map `T` of a Hilbert space is **positive** if it is self adjoint and
+  `∀ x, 0 ≤ re ⟪T x, x⟫`. -/
+def IsPositive (T : E →ₗ[𝕜] E) : Prop :=
+  IsSelfAdjoint T ∧ ∀ x, 0 ≤ re ⟪T x, x⟫
+
+theorem IsPositive.isSelfAdjoint {T : E →ₗ[𝕜] E} (hT : IsPositive T) :
+    IsSelfAdjoint T := hT.1
+
+theorem IsPositive.re_inner_nonneg_left {T : E →ₗ[𝕜] E} (hT : IsPositive T)
+    (x : E) : 0 ≤ re ⟪T x, x⟫ :=
+  hT.2 x
+
+theorem IsPositive.re_inner_nonneg_right {T : E →ₗ[𝕜] E} (hT : IsPositive T)
+    (x : E) : 0 ≤ re ⟪x, T x⟫ := by
+  rw [inner_re_symm]
+  exact hT.re_inner_nonneg_left x
+
+lemma isPositive_toContinuousLinearMap_iff [CompleteSpace E] (T : E →ₗ[𝕜] E) :
+    T.toContinuousLinearMap.IsPositive ↔ T.IsPositive := by
+  apply Iff.intro
+  · intro hT
+    apply And.intro
+    · exact (isSelfAdjoint_toContinuousLinearMap_iff T).mp hT.left
+    · intro x
+      have hx : 0 ≤ re ⟪T x, x⟫ := hT.right x
+      exact hx
+  · intro hT
+    apply And.intro
+    · exact (isSelfAdjoint_toContinuousLinearMap_iff T).mpr hT.left
+    · intro x
+      simp [ContinuousLinearMap.reApplyInnerSelf]
+      exact hT.right x
+
+lemma _root_.ContinuousLinearMap.isPositive_toLinearMap_iff [CompleteSpace E] (T : E →L[𝕜] E) :
+    (T : E →ₗ[𝕜] E).IsPositive ↔ T.IsPositive := by
+  apply Iff.intro
+  · intro hT
+    apply And.intro
+    · exact (isSelfAdjoint_toLinearMap_iff T).mp hT.left
+    · intro x
+      have hx : 0 ≤ re ⟪T x, x⟫ := hT.right x
+      exact hx
+  · intro hT
+    apply And.intro
+    · exact (isSelfAdjoint_toLinearMap_iff T).mpr hT.left
+    · intro x
+      have hx : 0 ≤ re ⟪T x, x⟫ := hT.right x
+      simp [hx]
+
+section Complex
+
+variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [FiniteDimensional ℂ E']
+
+theorem isPositive_iff_complex (T : E' →ₗ[ℂ] E') :
+    IsPositive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ := by
+  simp_rw [IsPositive, forall_and, ← isSymmetric_iff_isSelfAdjoint,
+    LinearMap.isSymmetric_iff_inner_map_self_real, conj_eq_iff_re]
+  rfl
+
+end Complex
+
+theorem IsPositive.isSymmetric {T : E →ₗ[𝕜] E} (hT : IsPositive T) :
+    IsSymmetric T := (isSymmetric_iff_isSelfAdjoint T).mpr hT.isSelfAdjoint
+
+open ComplexOrder in
+theorem isPositive_iff (T : E →ₗ[𝕜] E) :
+    IsPositive T ↔ IsSelfAdjoint T ∧ ∀ x, 0 ≤ ⟪T x, x⟫ := by
+  simp_rw [IsPositive, and_congr_right_iff, ← RCLike.ofReal_nonneg (K := 𝕜)]
+  intro hT
+  simp [isSymmetric_iff_isSelfAdjoint _ |>.mpr hT]
+
+open ComplexOrder in
+theorem IsPositive.inner_nonneg_left {T : E →ₗ[𝕜] E} (hT : IsPositive T) (x : E) : 0 ≤ ⟪T x, x⟫ :=
+  ((isPositive_iff T).mp hT).right x
+
+open ComplexOrder in
+theorem IsPositive.inner_nonneg_right {T : E →ₗ[𝕜] E} (hT : IsPositive T) (x : E) :
+    0 ≤ ⟪x, T x⟫ := by
+  rw [← hT.isSymmetric]
+  exact hT.inner_nonneg_left x
+
+@[simp]
+theorem isPositive_zero : IsPositive (0 : E →ₗ[𝕜] E) := ⟨.zero _, by simp⟩
+
+@[simp]
+theorem isPositive_one : IsPositive (1 : E →ₗ[𝕜] E) := ⟨.one _, fun _ => inner_self_nonneg⟩
+
+@[simp]
+theorem isPositive_natCast {n : ℕ} : IsPositive (n : E →ₗ[𝕜] E) := by
+  refine ⟨IsSelfAdjoint.natCast n, ?_⟩
+  intro x
+  simp only [Module.End.natCast_apply, ← Nat.cast_smul_eq_nsmul 𝕜, inner_smul_left, map_natCast,
+    mul_re, natCast_re, inner_self_im, mul_zero, sub_zero]
+  exact mul_nonneg n.cast_nonneg' inner_self_nonneg
+
+@[simp]
+theorem isPositive_ofNat {n : ℕ} [n.AtLeastTwo] : IsPositive (ofNat(n) : E →ₗ[𝕜] E) :=
+  isPositive_natCast
+
+@[aesop safe apply]
+theorem IsPositive.add {T S : E →ₗ[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) :
+    (T + S).IsPositive := by
+  refine ⟨hT.isSelfAdjoint.add hS.isSelfAdjoint, fun x => ?_⟩
+  rw [add_apply, inner_add_left, map_add]
+  exact add_nonneg (hT.re_inner_nonneg_left x) (hS.re_inner_nonneg_left x)
+
+@[aesop safe apply]
+theorem IsPositive.conj_adjoint {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (S : E →ₗ[𝕜] F) :
+    (S ∘ₗ T ∘ₗ S.adjoint).IsPositive := by
+  refine And.intro ?_ ?_
+  · rw [isSelfAdjoint_iff', adjoint_comp, adjoint_comp, adjoint_adjoint, ← star_eq_adjoint, hT.1]
+    rfl
+  · intro x
+    rw [comp_apply, ← adjoint_inner_right]
+    exact hT.re_inner_nonneg_left _
+
+@[aesop safe apply]
+theorem IsPositive.adjoint_conj {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (S : F →ₗ[𝕜] E) :
+    (S.adjoint ∘ₗ T ∘ₗ S).IsPositive := by
+  convert hT.conj_adjoint S.adjoint
+  rw [adjoint_adjoint]
+
+section PartialOrder
+
+/-- The (Loewner) partial order on linear maps on a Hilbert space determined by `f ≤ g`
+if and only if `g - f` is a positive linear map (in the sense of `LinearMap.IsPositive`). -/
+instance instLoewnerPartialOrder : PartialOrder (E →ₗ[𝕜] E) where
+  le f g := (g - f).IsPositive
+  le_refl _ := by simp
+  le_trans _ _ _ h₁ h₂ := by simpa using h₁.add h₂
+  le_antisymm f₁ f₂ h₁ h₂ := by
+    rw [← sub_eq_zero]
+    have h_isSymm := (isSymmetric_iff_isSelfAdjoint (f₁ - f₂)).mpr h₂.isSelfAdjoint
+    exact h_isSymm.inner_map_self_eq_zero.mp fun x ↦ by
+      open scoped ComplexOrder in
+      refine le_antisymm ?_ (h₂.inner_nonneg_left x)
+      rw [← neg_nonneg, ← inner_neg_left]
+      simpa using h₁.inner_nonneg_left x
+
+lemma le_def (f g : E →ₗ[𝕜] E) : f ≤ g ↔ (g - f).IsPositive := Iff.rfl
+
+lemma nonneg_iff_isPositive (f : E →ₗ[𝕜] E) : 0 ≤ f ↔ f.IsPositive := by
+  simpa using le_def 0 f
+
+end PartialOrder
+
+end LinearMap

Mathlib/Analysis/InnerProductSpace/StarOrder.lean

@@ -42,7 +42,7 @@ lemma IsPositive.spectrumRestricts {f : H →L[𝕜] H} (hf : f.IsPositive) :
         re_ofReal_mul, inner_self_eq_norm_sq, mul_comm]
     _ ≤ re ⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜 := by
       simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left]
-        using hf.inner_nonneg_left x
+        using hf.re_inner_nonneg_left x
     _ ≤ ‖⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜‖ := RCLike.re_le_norm _
 
 instance : NonnegSpectrumClass ℝ (H →L[𝕜] H) where

Mathlib/Analysis/InnerProductSpace/Symmetric.lean

@@ -127,6 +127,26 @@ theorem IsSymmetric.restrictScalars {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric)
     (T.restrictScalars ℝ).IsSymmetric :=
   fun x y => by simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]
 
+@[simp]
+theorem IsSymmetric.im_inner_apply_self {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :
+    im ⟪T x, x⟫ = 0 :=
+  conj_eq_iff_im.mp <| hT.conj_inner_sym x x
+
+@[simp]
+theorem IsSymmetric.im_inner_self_apply {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :
+    im ⟪x, T x⟫ = 0 := by
+  simp [← hT x x, hT]
+
+@[simp]
+theorem IsSymmetric.coe_re_inner_apply_self {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :
+    re ⟪T x, x⟫ = ⟪T x, x⟫ :=
+  conj_eq_iff_re.mp <| hT.conj_inner_sym x x
+
+@[simp]
+theorem IsSymmetric.coe_re_inner_self_apply {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :
+    re ⟪x, T x⟫ = ⟪x, T x⟫ := by
+  simp [← hT x x, hT]
+
 section Complex
 
 variable {V : Type*} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V]