Bell and Tsirelson inequalities

Stream: maths

[Scott Morrison]

Do you think I should try to change it? At the moment it seems to me that it's just going to be cumbersome to restrict the ordering to the self-adjoint elements, and somehow we don't lose anything by just having a partial order on everything.

[Kevin Buzzard]

Do you need an order on the complexes to talk about complex conjugation in this setting?

[Scott Morrison]

Yes, you do. The order you want is just the one that makes each horizontal line in the complex plane incomparable with each other line. Would that be unpleasant/wrong to have as an instance? If so, that suggests we should investigate only asking for an order on the self adjoint elements.

[Frédéric Dupuis]

Are you really using the order on elements where the imaginary part is nonzero?

[Frédéric Dupuis]

If having this as an instance doesn't cause problems elsewhere, that might make a lot of things simpler, like stating inequalities involving complex numbers that we know are always real.

[Scott Morrison]

No, I'm not using the order on non-self-adjoint elements at all.

[Scott Morrison]

It's a question of whether it's worth the encumbrance of having to define the subtype of self-adjoint elements, and put an order just on that, and then describe how the star interacts with that order.

Or to go with the current alternative, where it's much quicker to say how the order and the star structure should interact.

[Scott Morrison]

I guess I better try out making complex a star-ordered ring, and see if anything complains.

[Scott Morrison]

It seems making complex a star-ordered ring works fine.

[Frédéric Dupuis]

Excellent!

[Reid Barton]

This means $z \le w$ if $w - z$ is a nonnegative real number?

[Scott Morrison]

Yes.

[Frédéric Dupuis]

I just had a look at the bell branch -- looks good to me! Just one suggestion: what about changing has_star to:

class has_star (R S : Type u) :=
(star : R → S)

This way we could also use it for the adjoint of an operator of type E →L[𝕜] F.

[Scott Morrison]

Unfortunately I don't think that typeclass resolution is going to enjoy this problem of having to work out S every time. I will try it, but I'm pretty confident that this is a no-go.

[Frédéric Dupuis]

So even putting [has_star R R] instead of [has_star R] would cause problems...?

[Frédéric Dupuis]

Yeah, I guess having to define notation for every space to avoid this would just defeat the purpose. Never mind!