Zulip Chat Archive

Stream: maths

Topic: Bell and Tsirelson inequalities


view this post on Zulip Scott Morrison (Oct 03 2020 at 03:58):

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.

view this post on Zulip Kevin Buzzard (Oct 03 2020 at 08:19):

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

view this post on Zulip Scott Morrison (Oct 03 2020 at 10:48):

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.

view this post on Zulip Frédéric Dupuis (Oct 05 2020 at 22:55):

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

view this post on Zulip Frédéric Dupuis (Oct 05 2020 at 22:57):

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.

view this post on Zulip Scott Morrison (Oct 05 2020 at 23:19):

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

view this post on Zulip Scott Morrison (Oct 05 2020 at 23:21):

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.

view this post on Zulip Scott Morrison (Oct 05 2020 at 23:22):

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

view this post on Zulip Scott Morrison (Oct 06 2020 at 10:15):

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

view this post on Zulip Frédéric Dupuis (Oct 06 2020 at 19:34):

Excellent!

view this post on Zulip Reid Barton (Oct 06 2020 at 19:37):

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

view this post on Zulip Scott Morrison (Oct 06 2020 at 21:52):

Yes.

view this post on Zulip Frédéric Dupuis (Oct 09 2020 at 15:03):

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.

view this post on Zulip Scott Morrison (Oct 12 2020 at 03:45):

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.

view this post on Zulip Frédéric Dupuis (Oct 14 2020 at 15:58):

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

view this post on Zulip Frédéric Dupuis (Oct 14 2020 at 16:39):

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


Last updated: May 14 2021 at 20:13 UTC