[Merged by Bors] - refactor(Analysis/InnerProductSpace/Positive): generalize positivity to use IsSymmetric instead of IsSelfAdjoint and CompleteSpace

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -17,7 +17,7 @@ of requiring self adjointness in the definition.
 
 * `LinearMap.IsPositive` : a linear map is positive if it is symmetric and
   `∀ x, 0 ≤ re ⟪T x, x⟫`.
-* `ContinuousLinearMap.IsPositive` : a continuous linear map is positive if it is self adjoint and
+* `ContinuousLinearMap.IsPositive` : a continuous linear map is positive if it is symmetric and
   `∀ x, 0 ≤ re ⟪T x, x⟫`.
 
 ## Main statements
@@ -104,6 +104,9 @@ theorem isPositive_zero : IsPositive (0 : E →ₗ[𝕜] E) := ⟨.zero, by simp
 @[simp]
 theorem isPositive_one : IsPositive (1 : E →ₗ[𝕜] E) := ⟨.id, fun _ => inner_self_nonneg⟩
 
+@[simp]
+theorem isPositive_id : IsPositive (id : E →ₗ[𝕜] E) := isPositive_one
+
 @[simp]
 theorem isPositive_natCast {n : ℕ} : IsPositive (n : E →ₗ[𝕜] E) := by
   refine ⟨IsSymmetric.natCast n, fun x => ?_⟩
@@ -211,65 +214,77 @@ end LinearMap
 
 namespace ContinuousLinearMap
 
-variable [CompleteSpace E] [CompleteSpace F]
-
-/-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is self adjoint
+/-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is symmetric
   and `∀ x, 0 ≤ re ⟪T x, x⟫`. -/
 def IsPositive (T : E →L[𝕜] E) : Prop :=
-  IsSelfAdjoint T ∧ ∀ x, 0 ≤ T.reApplyInnerSelf x
+  T.IsSymmetric ∧ ∀ x, 0 ≤ T.reApplyInnerSelf x
 
-theorem IsPositive.isSelfAdjoint {T : E →L[𝕜] E} (hT : IsPositive T) : IsSelfAdjoint T :=
-  hT.1
+theorem isPositive_def {T : E →L[𝕜] E} :
+    T.IsPositive ↔ T.IsSymmetric ∧ ∀ x, 0 ≤ T.reApplyInnerSelf x := Iff.rfl
 
-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, hT.isSelfAdjoint.adjoint_eq]
+/-- In a complete space, a continuous linear endomorphism `T` is **positive** if it is
+symmetric and `∀ x, 0 ≤ re ⟪T x, x⟫`. -/
+theorem isPositive_def' [CompleteSpace E] {T : E →L[𝕜] E} :
+    T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ x, 0 ≤ T.reApplyInnerSelf x := by
+  simp [IsPositive, isSelfAdjoint_iff_isSymmetric, LinearMap.IsSymmetric]
 
-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.isSymmetric {T : E →L[𝕜] E} (hT : T.IsPositive) :
+    T.IsSymmetric := hT.1
 
-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
+theorem IsPositive.isSelfAdjoint [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsPositive T) :
+    IsSelfAdjoint T := hT.isSymmetric.isSelfAdjoint
+
+theorem IsPositive.inner_left_eq_inner_right {T : E →L[𝕜] E} (hT : IsPositive T) (x y : E) :
+    ⟪T x, y⟫ = ⟪x, T y⟫ := hT.isSymmetric _ _
+
+theorem IsPositive.re_inner_nonneg_left {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
+    0 ≤ re ⟪T x, x⟫ := hT.2 x
 
-omit [CompleteSpace E] in
 lemma _root_.LinearMap.isPositive_toContinuousLinearMap_iff
     [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :
-    have : CompleteSpace E := FiniteDimensional.complete 𝕜 _
-    T.toContinuousLinearMap.IsPositive ↔ T.IsPositive := by
-  simp only [IsPositive, isSelfAdjoint_iff_isSymmetric, coe_toContinuousLinearMap, reApplyInnerSelf,
-    coe_toContinuousLinearMap', LinearMap.IsPositive]
+    T.toContinuousLinearMap.IsPositive ↔ T.IsPositive := Iff.rfl
 
 lemma isPositive_toLinearMap_iff (T : E →L[𝕜] E) :
-    (T : E →ₗ[𝕜] E).IsPositive ↔ T.IsPositive := by
-  simp only [LinearMap.IsPositive, ← isSelfAdjoint_iff_isSymmetric, coe_coe, IsPositive,
-    reApplyInnerSelf]
+    (T : E →ₗ[𝕜] E).IsPositive ↔ T.IsPositive := Iff.rfl
 
 alias ⟨_, IsPositive.toLinearMap⟩ := isPositive_toLinearMap_iff
 
+theorem IsPositive.re_inner_nonneg_right {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
+    0 ≤ re ⟪x, T x⟫ := hT.toLinearMap.re_inner_nonneg_right x
+
 open ComplexOrder in
+/-- An operator is positive iff it is symmetric and `0 ≤ ⟪T x, x⟫`.
+
+For the version with `IsSelfAdjoint` instead of `IsSymmetric`, see
+`ContinuousLinearMap.isPositive_iff'`. -/
 theorem isPositive_iff (T : E →L[𝕜] E) :
+    IsPositive T ↔ T.IsSymmetric ∧ ∀ x, 0 ≤ ⟪T x, x⟫ := LinearMap.isPositive_iff _
+
+open ComplexOrder in
+/-- An operator is positive iff it is self-adjoint and `0 ≤ ⟪T x, x⟫`.
+
+For the version with `IsSymmetric` instead of `IsSelfAdjoint`, see
+`ContinuousLinearMap.isPositive_iff`. -/
+theorem isPositive_iff' [CompleteSpace E] (T : E →L[𝕜] E) :
     IsPositive T ↔ IsSelfAdjoint T ∧ ∀ x, 0 ≤ ⟪T x, x⟫ := by
-  simp [← isPositive_toLinearMap_iff, isSelfAdjoint_iff_isSymmetric, LinearMap.isPositive_iff]
+  simp [isSelfAdjoint_iff_isSymmetric, isPositive_iff]
 
 open ComplexOrder in
 theorem IsPositive.inner_nonneg_left {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
-    0 ≤ ⟪T x, x⟫ :=
-  (T.isPositive_iff.mp hT).right x
+    0 ≤ ⟪T x, x⟫ := hT.toLinearMap.inner_nonneg_left x
 
 open ComplexOrder in
 theorem IsPositive.inner_nonneg_right {T : E →L[𝕜] E} (hT : IsPositive T) (x : E) :
-    0 ≤ ⟪x, T x⟫ := by
-  rw [← hT.inner_left_eq_inner_right]
-  exact inner_nonneg_left hT x
+    0 ≤ ⟪x, T x⟫ := hT.toLinearMap.inner_nonneg_right x
 
 @[simp]
-theorem isPositive_zero : IsPositive (0 : E →L[𝕜] E) :=
-  (isPositive_toLinearMap_iff _).mp LinearMap.isPositive_zero
+theorem isPositive_zero : IsPositive (0 : E →L[𝕜] E) := LinearMap.isPositive_zero
 
 @[simp]
-theorem isPositive_one : IsPositive (1 : E →L[𝕜] E) :=
-  ⟨.one _, fun _ => inner_self_nonneg⟩
+theorem isPositive_id : IsPositive (id 𝕜 E : E →L[𝕜] E) := LinearMap.isPositive_id
+
+@[simp]
+theorem isPositive_one : IsPositive (1 : E →L[𝕜] E) := LinearMap.isPositive_one
 
 @[simp]
 theorem isPositive_natCast {n : ℕ} : IsPositive (n : E →L[𝕜] E) :=
@@ -291,30 +306,27 @@ theorem IsPositive.smul_of_nonneg {T : E →L[𝕜] E} (hT : T.IsPositive) {c :
   (isPositive_toLinearMap_iff _).mp (hT.toLinearMap.smul_of_nonneg hc)
 
 @[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 => ?_⟩
+theorem IsPositive.conj_adjoint [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E}
+    (hT : T.IsPositive) (S : E →L[𝕜] F) : (S ∘L T ∘L S†).IsPositive := by
+  refine isPositive_def'.mpr ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩
   rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]
   exact hT.re_inner_nonneg_left _
 
-theorem isPositive_self_comp_adjoint (S : E →L[𝕜] F) :
+theorem isPositive_self_comp_adjoint [CompleteSpace E] [CompleteSpace F] (S : E →L[𝕜] F) :
     (S ∘L S†).IsPositive := by
   simpa using isPositive_one.conj_adjoint S
 
 @[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
+theorem IsPositive.adjoint_conj [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E}
+    (hT : T.IsPositive) (S : F →L[𝕜] E) : (S† ∘L T ∘L S).IsPositive := by
   convert hT.conj_adjoint (S†)
   rw [adjoint_adjoint]
 
-theorem isPositive_adjoint_comp_self (S : E →L[𝕜] F) :
+theorem isPositive_adjoint_comp_self [CompleteSpace E] [CompleteSpace F] (S : E →L[𝕜] F) :
     (S† ∘L S).IsPositive := by
   simpa using isPositive_one.adjoint_conj S
 
 section LinearMap
-
-omit [CompleteSpace E] [CompleteSpace F]
-
 variable [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F]
 
 @[aesop safe apply]
@@ -344,13 +356,19 @@ end LinearMap
 theorem IsPositive.conj_starProjection (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : T.IsPositive)
     [U.HasOrthogonalProjection] :
     (U.starProjection ∘L T ∘L U.starProjection).IsPositive := by
-  have := hT.conj_adjoint (U.starProjection)
-  rwa [(isSelfAdjoint_starProjection U).adjoint_eq] at this
+  simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
+    Function.comp_apply, coe_comp']
+  simp_rw [← coe_coe, U.starProjection_isSymmetric _ , hT.isSymmetric _,
+    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
+    hT.inner_nonneg_right, implies_true, and_self]
 
 theorem IsPositive.orthogonalProjection_comp {T : E →L[𝕜] E} (hT : T.IsPositive) (U : Submodule 𝕜 E)
-    [CompleteSpace U] : (U.orthogonalProjection ∘L T ∘L U.subtypeL).IsPositive := by
-  have := hT.conj_adjoint (U.orthogonalProjection : E →L[𝕜] U)
-  rwa [U.adjoint_orthogonalProjection] at this
+    [U.HasOrthogonalProjection] : (U.orthogonalProjection ∘L T ∘L U.subtypeL).IsPositive := by
+  simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
+    Function.comp_apply, coe_comp']
+  simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
+    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
+    hT.inner_nonneg_right, implies_true, and_self]
 
 open scoped NNReal
 
@@ -365,7 +383,7 @@ lemma antilipschitz_of_forall_le_inner_map {H : Type*} [NormedAddCommGroup H]
   · apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff.mpr hx0)).mp
     exact (h x).trans <| (norm_inner_le_norm _ _).trans <| (mul_comm _ _).le
 
-lemma isUnit_of_forall_le_norm_inner_map (f : E →L[𝕜] E) {c : ℝ≥0} (hc : 0 < c)
+lemma isUnit_of_forall_le_norm_inner_map [CompleteSpace E] (f : E →L[𝕜] E) {c : ℝ≥0} (hc : 0 < c)
     (h : ∀ x, ‖x‖ ^ 2 * c ≤ ‖⟪f x, x⟫_𝕜‖) : IsUnit f := by
   rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]
   have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h
@@ -377,8 +395,7 @@ lemma isUnit_of_forall_le_norm_inner_map (f : E →L[𝕜] E) {c : ℝ≥0} (hc
   aesop
 
 section Complex
-
-variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [CompleteSpace E']
+variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace ℂ E']
 
 theorem isPositive_iff_complex (T : E' →L[ℂ] E') :
     IsPositive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ := by
@@ -411,7 +428,7 @@ end PartialOrder
 
 /-- An idempotent operator is positive if and only if it is self-adjoint. -/
 @[grind →]
-theorem IsIdempotentElem.isPositive_iff_isSelfAdjoint
+theorem IsIdempotentElem.isPositive_iff_isSelfAdjoint [CompleteSpace E]
     {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : p.IsPositive ↔ IsSelfAdjoint p := by
   rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap]
   exact isSelfAdjoint_iff_isSymmetric.symm
@@ -421,7 +438,7 @@ theorem IsIdempotentElem.isPositive_iff_isSelfAdjoint
 The proof of this will soon be simplified to `IsStarProjection.nonneg` when we
 have `StarOrderedRing (E →L[𝕜] E)`. -/
 @[aesop 10% apply, grind →]
-theorem IsPositive.of_isStarProjection {p : E →L[𝕜] E}
+theorem IsPositive.of_isStarProjection [CompleteSpace E] {p : E →L[𝕜] E}
     (hp : IsStarProjection p) : p.IsPositive :=
   hp.isIdempotentElem.isPositive_iff_isSelfAdjoint.mpr hp.isSelfAdjoint
 
@@ -430,7 +447,7 @@ theorem IsPositive.of_isStarProjection {p : E →L[𝕜] E}
 * `p` is normal
 * `p` is self-adjoint
 * `p` is positive -/
-theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) :
+theorem IsIdempotentElem.TFAE [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) :
     [(LinearMap.range p)ᗮ = LinearMap.ker p,
       IsStarNormal p,
       IsSelfAdjoint p,

Mathlib/Analysis/InnerProductSpace/StarOrder.lean

@@ -58,8 +58,8 @@ lemma instStarOrderedRingRCLike
     constructor
     · intro h
       rw [le_def] at h
-      obtain ⟨p, hp₁, -, hp₃⟩ :=
-        CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.spectrumRestricts
+      obtain ⟨p, hp₁, -, hp₃⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts
+        h.isSelfAdjoint h.spectrumRestricts
       refine ⟨p ^ 2, ?_, by symm; rwa [add_comm, ← eq_sub_iff_add_eq]⟩
       exact AddSubmonoid.subset_closure ⟨p, by simp only [hp₁.star_eq, sq]⟩
     · rintro ⟨p, hp, rfl⟩