Supp addition on LinearMaps Properties

Stream: Is there code for X?

[Jam Kabeer Ali Khan]

I am trying to formalize the following two lemmas, and I wanted to ask if these are present in MathLib?

lemma ker_add (P Q : E →ₗ[𝕜] E) (hP : LinearMap.isPositiveSemiDefinite P) (hQ : LinearMap.isPositiveSemiDefinite Q):
  (LinearMap.ker (P + Q)) = (LinearMap.ker P) ⊓ (LinearMap.ker Q)

The above states that ker of the sum of two positive-semidefinite operators must be equal to the intersection of the kernels of individual operators.
I am also proving the property below:

lemma ker_union (P Q : E →ₗ[𝕜] E) (hP : LinearMap.isPositiveSemiDefinite P) (hQ : LinearMap.isPositiveSemiDefinite Q):
  (LinearMap.ker P ⊓ LinearMap.ker Q)ᗮ = (LinearMap.ker P)ᗮ ⊔ (LinearMap.ker Q)ᗮ

For the first property, I am trying to prove by cases on the fact that P and Q are positive semi-definite, which has below definition

/-- Positive semidefinite operators. -/
def isPositiveSemiDefinite (T : E →ₗ[𝕜] E) : Prop :=
  IsSelfAdjoint T ∧ ∀ x, 0 ≤ RCLike.re (inner (T x) x : 𝕜)

But I am stuck on showing the contradiction in one of the cases.
Is there code for this property in MathLib for positive semi-definite operators? Thank you!

[Jam Kabeer Ali Khan]

here are the proof states I am stuck at

P Q : E →ₗ[𝕜] E
hP_self : IsSelfAdjoint P
hP_re : ∀ (x : E), 0 ≤ RCLike.re (inner (P x) x)
hQ_self : IsSelfAdjoint Q
hQ_re : ∀ (x : E), 0 ≤ RCLike.re (inner (Q x) x)
x : E
this : RCLike.re (inner (P x) x) + RCLike.re (inner (Q x) x) = 0
h : P x + Q x = 0
hPx : RCLike.re (inner (P x) x) = 0
hQx : RCLike.re (inner (Q x) x) = 0
inner_Px : inner (P x) x = 0
inner_Qx : inner (Q x) x = 0
⊢ P x = 0 ∧ Q x = 0

[Kevin Buzzard]

(a) do you know the maths proof and (b) can you make a #mwe ?

[Jam Kabeer Ali Khan]

a)
Math proofs follow from the fact that P and Q are positive semi-definite operators, and that

<x|P|x> + <x|Q|x> = <x|P*P|x| + <x|Q*Q|x> = ||Px|| + ||Qx|| = 0 => Px = 0 and Qx = 0

Above is for ker_add
And the ker_union seems to follow from De Morgan

This is my understanding, but I might be wrong.

b) here is #mwe

import Mathlib.Analysis.InnerProductSpace.Positive

variable {𝕜 E : Type*} [RCLike 𝕜]

variable? [HilbertSpace 𝕜 E] => [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
variable [FiniteDimensional 𝕜 E]

namespace LinearMap
/-- Positive semidefinite operators. -/
def isPositiveSemiDefinite (T : E →ₗ[𝕜] E) : Prop :=
  IsSelfAdjoint T ∧ ∀ x, 0 ≤ RCLike.re (inner 𝕜 (T x) x)
end LinearMap

namespace SupportProp

def supp (P : E →ₗ[𝕜] E) : Submodule 𝕜 E := (LinearMap.ker P)ᗮ

lemma ker_add (P Q : E →ₗ[𝕜] E) (hP : LinearMap.isPositiveSemiDefinite P) (hQ : LinearMap.isPositiveSemiDefinite Q):
  (LinearMap.ker (P + Q)) = (LinearMap.ker P) ⊓ (LinearMap.ker Q)               := by
  sorry

lemma ker_union (P Q : E →ₗ[𝕜] E) (hP : LinearMap.isPositiveSemiDefinite P) (hQ : LinearMap.isPositiveSemiDefinite Q):
  (LinearMap.ker P ⊓ LinearMap.ker Q)ᗮ = (LinearMap.ker P)ᗮ ⊔ (LinearMap.ker Q)ᗮ := by
  sorry

lemma supp_add (P Q : E →ₗ[𝕜] E) (hP : LinearMap.isPositiveSemiDefinite P) (hQ : LinearMap.isPositiveSemiDefinite Q) :
    supp (P + Q) = supp (P) ⊔ supp (Q)  := by
    rw [supp, supp, supp, ker_add, ker_union]
    · apply hP
    · apply hQ
    · apply hP
    · apply hQ
end SupportProp

Apologies for not giving #mwe earlier; thanks a lot!