Positive-semidefinite linear operator

Stream: Is there code for X?

[Iván Renison]

Hi, I was trying to have positive-semidefinite linear operators for an 𝕜 : RCLike.
I found the definition Matrix.PosSemidef, but it requires PartialOrder 𝕜.
Because of that I thought in using linear maps, and I came up with this definition:

def isPosSemidef (f : E → E) (h : IsLinearMap 𝕜 f) : Prop :=
  ∀ (x : E), RCLike.im (inner x (f x) : 𝕜) = 0 ∧ 0 ≤ RCLike.re (inner x (f x) : 𝕜)

But I was not able to find anything similar in Mathlib, do you now if it is somewhere? And if not, would it be a good addition?

[Eric Wieser]

docs#ContinuousLinearMap.IsPositive is close

[Eric Wieser]

Iván Renison said:

but it requires PartialOrder 𝕜.

open scoped ComplexOrder

[Iván Renison]

Thanks

[Notification Bot]

Iván Renison has marked this topic as resolved.

[Jireh Loreaux]

Note we have docs#ContinuousLinearMap.instLoewnerPartialOrder

[Notification Bot]

Iván Renison has marked this topic as unresolved.

[Iván Renison]

Eric Wieser said:

docs#ContinuousLinearMap.IsPositive is close

And do you now if there si something for LinearMap instead of ContinuousLinearMap?
I think it is possible to define like this:

def LinearMap.aux_IsPositive (T : E →ₗ[𝕜] E) : Prop :=
  IsSelfAdjoint T ∧ ∀ x, 0 ≤ RCLike.re (@inner 𝕜 _ _ (T x) x)

But I can not see it in Mathlib, so maybe it's wrong

[Jireh Loreaux]

It's possible that from a discussion long ago I advocated against this, and that's why we don't have it.

[Jireh Loreaux]

But I wouldn't advocate against it now necessarily.

[Iván Renison]

And would you encourage me to add it now? Or better let it how it is

[Eric Wieser]

Jireh Loreaux said:

It's possible that from a discussion long ago I advocated against this, and that's why we don't have it.

I think there was a PR adding this, possibly in mathlib3

[Eric Wieser]

We should probably find it and read over the old discussions before rehashing it

[Iván Renison]

I'm not being able to find it

[Eric Wieser]

!3#18230

[Iván Renison]

What I understand from that conversation is that the idea was to make a definition of isPositivefor a general Star algebra, defining it as x is positive if there exists y such that x = star y * y. However, it seems that this hasn't been added yet

[Jireh Loreaux]

I think it's okay to have LinearMap.IsPositive.

[Eric Wieser]

I think when we had this discussion previously, StarOrderedRing wasn't as developed; should we instead just put a global order on linear maps in an inner product space?

[Iván Renison]

That looks like a good idea to reuse the theorems

[Iván Renison]

But if we do that, I think we should also do it for ContinuousLinearMap also

[Jireh Loreaux]

We already have it for ContinuousLinearMap, but the partial order is defined in terms of ContinuousLinearMap.IsPositive. This is partly why I'm suggesting having the predicate isn't so crazy anymore.

[Jireh Loreaux]

docs#ContinuousLinearMap.instLoewnerPartialOrder

[Jireh Loreaux]

docs#ContinuousLinearMap.instStarOrderedRing

[Jireh Loreaux]

Note that we only have the latter over ℂ because we don't yet have a theory of real C⋆-algebras from which we can easily construct the square root. It would be possible to hand roll the square root by embedding H →L[ℝ] H into its complexification and then proving that for a T : H →L[ℝ] H selfadjoint, the closed ℝ-star subalgebra generated by T remains within the image of H →L[ℝ] H embedded within the complexification, and hence the square root of T (if T ≥ 0) lies in H →L[ℝ] H. But I think this is too much work to pursue and we should instead simply develop real C⋆-algebras. It's on my agenda, but not for a long time, since so much of the real theory depends upon the complex theory.