(anti)-monotone

Stream: maths

[Johan Commelin]

@Damiano Testa needs non-increasing maps: https://github.com/leanprover-community/mathlib/pull/4707/files#diff-7988ec8f11293ebdbc60170c32d15458910725a0f10ee3333b5b60134e745ccaR23

We've talked a lot about this before. I think we should find some definitive solution, and implement it. (Either code, or guidelines on what to do.) Options that I see:

1. Define a predicate for non-increasing maps
2. Use the dual order.
3. Use some rel_hom.

@Yury G. Kudryashov @Mario Carneiro @Aaron Anderson
(I think Aaron did something with (3) recently, but I'm not up to speed with what's there and what works.)

[Mario Carneiro]

I would like 2 to at least be usable

[Damiano Testa]

Thanks for the thread!

I tried 2, but was unable to get Lean to accept that the same type (\N in my case) had two different orders... This is my inability and it can probably be done already, but I do not know how...

[Johan Commelin]

@Damiano Testa I think there is a dual_order type synonym. Or maybe it is called order_dual?

[Damiano Testa]

I got to the stage where I realized, I think, that order_dual X (or something similar) was simply a type synonym for X but I was not able to give it the opposite order...

[Mario Carneiro]

it should already exist

[Damiano Testa]

src/order/basic.lean

As far as I understand, order_dual X is a type synonym for X. How do I produce an X' that is "X with the dual order"? I believe that this is simply a question of what command to give Lean, since in the cited file dual_le seems to exactly be the mathematical "dual order".

[Mario Carneiro]

There should be a to_dual function that is a synonym for the identity function

[Mario Carneiro]

Er, wait are you asking how to make a type that is "X with the dual order"? That's order_dual X

[Mario Carneiro]

it is a type synonym for X but it's order is the dual order

[Damiano Testa]

Ok, maybe this is not literally what I meant. I would like to "use the dual order on X", but Lean keeps using the "usual" order on X, even if I call it order_dual X. Is this clearer?

[Mario Carneiro]

If you have a b : order_dual X and write a <= b, that will come out the same as b <= a in the order on X

[Damiano Testa]

I will try again: maybe I got confused and Lean was doing the right thing, but I did not have it straight in my mind.

[Damiano Testa]

Mario Carneiro said:

If you have a b : order_dual X and write a <= b, that will come out the same as b <= a in the order on X

Ok, this is exactly what I want: I will try again!

[Mario Carneiro]

If you have a b : X and write (a : order_dual X) <= b though, it will still come out as a <= b

[Mario Carneiro]

which is why it's useful to have an identity function here: if you write @id (order_dual X) a <= @id (order_dual X) b then that comes out as b <= a

[Damiano Testa]

Mario Carneiro said:

which is why it's useful to have an identity function here: if you write @id (order_dual X) a <= @id (order_dual X) b then that comes out as b <= a

I believe that this is exactly the command that I was missing!

[Mario Carneiro]

Usually we define to_dual : X -> order_dual X := id and then use to_dual instead of that @id application

[Mario Carneiro]

but I don't know if that's in the library

[Damiano Testa]

I had produced a new type with an order and defined an "order reversing function". Now I should be able to use the order_dual type and this @id (order_dual X)

[Damiano Testa]

Mario Carneiro said:

Usually we define to_dual : X -> order_dual X := id and then use to_dual instead of that @id application

I searched for "to_dual" and it was not in the file above.

[Mario Carneiro]

Our practices in defining type synonyms have changed over the years

[Mario Carneiro]

see for example src#opposite.op

[Mario Carneiro]

It's possible to avoid using these identity functions, but you have to assert a lot more type annotations and you get more "leakage" of the instance from X instead of order_dual X

[Damiano Testa]

I was not expecting to find a to_dual, since I am not sure yet what to expect with Lean! However, what you mentioned is highly likely to solve my problems!

[Damiano Testa]

I seem to have the same problem: I would like the min' to be computed using the dual order, but it seems to be still the old order...

import data.finsupp.basic

def to_dual (α : Type*) [linear_order α] : α -> order_dual α := id

lemma monotone_max'_min' {α : Type*} [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
  max' s hs = (min' (image (to_dual α) s) (nonempty.image hs (to_dual α))) :=
begin
  sorry,
end

[Johan Commelin]

You probably want

import data.finsupp.basic

open finset

variables {α : Type*}

def to_dual : α → order_dual α := id

def of_dual : order_dual α → α := id

lemma monotone_max'_min' [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
  max' s hs = of_dual (min' (image to_dual s) (nonempty.image hs to_dual)) :=
begin

end

[Damiano Testa]

(In case it is helpful, this is my earlier question on the topic:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/monotone.20decreasing.20.60.60.60.E2.84.95.20.E2.86.92.20.E2.84.95.60.60.60)

[Johan Commelin]

@Damiano Testa In your example, Lean was looking at the =, and thinking

hmmm, where does this = live? Let's look at the LHS: max' s hs. Ok, that's in \alpha. So then the RHS must also live in \alpha, so I'm going to take that min' in \alpha with the order coming from \alpha.
Aah, I see that the user wrote to_dual, but I'm going to ignore that.

[Damiano Testa]

@Johan Commelin thanks for the explanation! I will use your code!

[Johan Commelin]

Because I added the of_dual in front of the RHS, Lean will think

Ok, so the RHS has to live in \alpha. That means that the argument to of_dual must live in order_dual \alpha. Let me take the min' in the order dual of \alpha.

[Scott Morrison]

Yes, please define, if they don't exist already, explicit to_dual and of_dual functions, and use those. Ideally after defining those you can mark order_dual as [irreducible], which will guard against "accidentally" changing between the type and its order_dual.

[Johan Commelin]

This still breaks through a little bit of abstraction. But it is a start.

import data.finsupp.basic

open finset

variables {α : Type*}

def to_dual : α → order_dual α := id

def of_dual : order_dual α → α := id

@[simp] lemma to_dual_of_dual (a : order_dual α) : to_dual (of_dual a) = a := rfl
@[simp] lemma of_dual_to_dual (a : α) : of_dual (to_dual a) = a := rfl

section

lemma to_dual_injective : function.injective (to_dual : α → order_dual α) :=
function.injective_id

@[simp] lemma to_dual_inj {a b : α} :
  to_dual a = to_dual b ↔ a = b := iff.rfl

@[simp] lemma to_dual_le_to_dual [has_le α] {a b : α} :
  to_dual a ≤ to_dual b ↔ b ≤ a := iff.rfl

@[simp] lemma to_dual_lt_to_dual [has_lt α] {a b : α} :
  to_dual a < to_dual b ↔ b < a := iff.rfl

lemma of_dual_injective : function.injective (of_dual : order_dual α → α) :=
function.injective_id

@[simp] lemma of_dual_inj {a b : order_dual α} :
  of_dual a = of_dual b ↔ a = b := iff.rfl

@[simp] lemma of_dual_le_of_dual [has_le α] {a b : order_dual α} :
  of_dual a ≤ of_dual b ↔ b ≤ a := iff.rfl

@[simp] lemma of_dual_lt_of_dual [has_lt α] {a b : order_dual α} :
  of_dual a < of_dual b ↔ b < a := iff.rfl

lemma le_to_dual [has_le α] {a : order_dual α} {b : α} :
  a ≤ to_dual b ↔ b ≤ of_dual a := iff.rfl

lemma lt_to_dual [has_lt α] {a : order_dual α} {b : α} :
  a < to_dual b ↔ b < of_dual a := iff.rfl

lemma to_dual_le [has_le α] {a : α} {b : order_dual α} :
  to_dual a ≤ b ↔ of_dual b ≤ a := iff.rfl

lemma to_dual_lt [has_lt α] {a : α} {b : order_dual α} :
  to_dual a < b ↔ of_dual b < a := iff.rfl

end

lemma monotone_max'_min' [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
  max' s hs = of_dual (min' (image to_dual s) (nonempty.image hs to_dual)) :=
begin
  apply le_antisymm,
  { apply max'_le,
    intros,
    rw [← le_to_dual],
    apply min'_le,
    rw [mem_image],
    refine ⟨_, H, rfl⟩ },
  { rw [← to_dual_le],
    apply le_min',
    intros,
    rw [to_dual_le],
    apply le_max',
    rw mem_image at H,
    rcases H with ⟨x, H, rfl⟩,
    exact H }
end

[Mario Carneiro]

the last proof would be simpler if you prove of_dual (min' x y) = max' (of_dual x) (of_dual y) and variations

[Mario Carneiro]

well, I guess that's already what it is

[Damiano Testa]

@Johan Commelin
Thank you for spelling everything out for me!

What I needed indeed was the statement that max' and min' are exchanged after going through the order dual! I was going to prove as an exercise the analogous statement about max and min of individual elements, but I had to leave and left all for later!

[Yury G. Kudryashov]

@Damiano Testa max and min are defined so that max a b = min (to_dual a) (to_dual b) is a rfl.

[Yury G. Kudryashov]

I think that we should rename monotone to mono_incr and define mono_decr.

[Yury G. Kudryashov]

mono_decr α β should be defeq mono_incr α (order_dual β)

[Yury G. Kudryashov]

def mono_decr f := ∀ {{x y}}, x ≤ y → f y ≤ f x

[Yury G. Kudryashov]

Most proofs about mono_decr should be := @(thm_about_mono_incr) _ (order_dual _) _ _ _

[Yury G. Kudryashov]

See strict_mono_decr_on for an example.

[Kevin Buzzard]

In general mathlib has got a very long way with its philosophy that the nicest structures and ideas are the ones which preserve notation. For example we have a gigantic theory about functions satisfying f(a+b)=f(a)+f(b). On the other hand it seems we have essentially nothing about functions satisfying f(a*b)=f(a)+f(b), because we have noticed that the mathematician's conventions for addition and multiplication often seem to be going on in some kind of consistent and compatible way (surprise surprise) -- but not always (see e.g. additive valuations, which don't exist in mathlib yet). There is some kind of "exponential / log" bridge which takes you from the multiplicative to the additive structure and back, but we don't have a general class of functions with this property, we just have multiplicative.to_add and are expected to build everything upon that.

The argument against adding some kind of +→* notation is that "it won't scale". Fortunately, in the 2000 years since we've known about + and * we've not invented any more fundamental operations which are valid in vast generality, so these things won't have to scale much. The ever-increasing pile of -> and \equiv notation is of course a bit disturbing (and makes mathlib harder to read for mathematicians with no background), but this is perhaps a different question.

I've always thought of this <= v >= thing as being a similar sort of thing. Thus far we have stuck with the order-preserving concept monotone, and because the universe is in some sort of harmony we've been able to get a long way with it. However there is this fundamental fact that if <= is a partial order then so is >=, and furthermore in the kind of MSc level stuff we're doing now we do see this duality showing up; many natural constructions relating algebra and geometry e.g. the contravariant Galois connection between subsets of affine n-space and subsets of polynomial rings (subspace goes to functions vanishing on the subspace; set of functions goes to subset where they all vanish) (edit: perhaps it's also worth mentioning Galois' original Galois connection! An order-reversing one between subsets of a field and subsets of a Galois group, a very natural example of a mono_decr and one which we will be needing very soon in mathlib). Thus far we've been expected to rely on order_dual and do everything by hand, but one wonders whether now it is time to experiment with these classes which don't preserve a notation but instead map it to another notation. I'm definitely for the experiment.

[Damiano Testa]

I have read your suggestions, and I am happy with them! I just do not trust my understanding of Lean enough to actually perform such a major revision of monotone. What I needed was really just the proof above. I will try to see @Johan Commelin's solution using order_duals but already the comment about irreducible is very opaque to me...

[Kevin Buzzard]

Those of us who don't want these hybrid functions will end up having to ask for the monoid hom exp' : multiplicative(real) -> real because they will be restricted to the classes that we currently have. Similarly if we don't inroduce this then we'll end up with subfields -> order_dual (subgroups) in Galois theory, and perhaps order_dual(subgroups) -> subfields as well (even moving between those two "identical" maps will be a slight pain, and of course we have the same question for the inverses). With this proposal we just get one mono_decr.

[Kevin Buzzard]

@Damiano Testa Mathlib is "weird" when it comes to groups. The founders decided to set up the entire theory twice, once with group for group law * and once with add_group with group law +. On the face of it, this sounds like a terrible idea! I think it came out of the way notation is used in typeclasses. But actually it seems to work fine in practice. However it does mean that the concept of an isomorphism between a multiplicative and an additive group is a new concept, different to isomorphisms of multiplicative groups (which we have already). We have sort of been resisting making these bridges and this is what has held up valuations on a DVR (that and the fact that I had to make a whole bunch of vlogs for the new Imperial students, something which has taken me 6 weeks of solid work). I now know what I'm doing (I'm just going to mimic what Rob did for p-adic valuations) but this doesn't mean that that questions go away in general. A lot of stuff is order-reversing once you start doing algebraic geometry. Yury is just suggesting hard coding some special case of a contravariant functor to see if it makes life better -- instead of being a covariant functor to the dual category (or is it from the dual category? Same thing to us, different thing to Lean), it's perhaps time to experiment directly. This stuff has all come up before, and people have just been playing with what to do about it in general.

[Damiano Testa]

I am perfectly happy with having commands for monotone_decreasing! Most of the PRs that I put in were to deal with trailing_coefficients which is simply the leading_coefficients for the opposite order!! So I am all in favour of making this a simpler procedure! I just had no idea where to start. Now, I think that I know where to start, but do not feel that I am able to produce code like the one that @Johan Commelin produced as quickly and efficiently...

[Kevin Buzzard]

yes, setting up the foundations should perhaps be done by an expert.

[Damiano Testa]

Could I suggest making a PR with the code that @Johan Commelin wrote above in a separate file in the order folder, maybe in a file called mon_decr.lean, so that #4707 can then proceed? The lemma there is the only "monotone-decreasing" information that I need...

[Johan Commelin]

I think that apart from the min-max lemma, all the stuff that I wrote should be close to the definition of order_dual

[Johan Commelin]

The min-max lemma can probably go close to the definition of min' and max'

[Damiano Testa]

In case you are interested, I created this PR: #4715. I simply merged @Johan Commelin 's code where it seemed appropriate!

[Johan Commelin]

@Damiano Testa I think the monotone_max'_min' should get a different name, though

[Johan Commelin]

And we need a different reviewer, because I wrote too much of this PR

[Johan Commelin]

Also, I think you don't need the linear order assumption, right?

[Johan Commelin]

Under which assumptions are min' and max' defined? I dunno

[Damiano Testa]

Johan Commelin said:

Damiano Testa I think the monotone_max'_min' should get a different name, though

max'_eq_dual_min'?

[Johan Commelin]

I think that's better

[Damiano Testa]

Maybe we can reverse the equality and think of it as a simp lemma?

[Damiano Testa]

(and call it dual_min'_eq_max')

[Mario Carneiro]

@Kevin Buzzard I agree that antitone functions or whatever we call them are important and on a fairly short list of permutations on the symbols we have available so there isn't too much risk of combinatorial growth, but I would still like to see it grow "organically", waiting until we have a critical mass of theorems about order_dual homs so that we know what's important

[Mario Carneiro]

I think the max/min simp lemmas should be of_dual (max a b) = min (of_dual a) (of_dual b) and the four variations on this with min/max swapped and to_dual instead of of_dual

[Yury G. Kudryashov]

@Johan Commelin If you carefully define max' and min', then the duality is a rfl.

[Johan Commelin]

But then we need to redefine them, I guess?

[Yury G. Kudryashov]

Where are they defined? I'm on the phone.

[Yury G. Kudryashov]

I've redefined min and max in stdlib to get rfl some time ago

[Heather Macbeth]

I would like to flag an analogy: working with anti-monotone functions as monotone functions for the order-dual (defined via a type synonym) on one of the sets, is quite similar to what @Frédéric Dupuis is currently working on in #4379, working with conjugate-linear maps as linear maps for the conjugate-space (defined via a type synonym) of one of the two vector spaces.

[Heather Macbeth]

I haven't had time to read this thread and think through whether there are any lessons that can be taken from it for @Frédéric Dupuis ' situation (or vice versa). But I'll try later (or maybe someone more experienced can do so immediately).

[Frédéric Dupuis]

To add a bit more details: #4379 basically introduces the dual of a Hilbert space, and we want to show that the map that takes a vector to its dual is semilinear. Since we don't have semilinear maps, we can instead view it as a linear map from the conjugate vector space to the dual, so conjugate vector spaces are also defined there as a type synonym with the right instances.

[Frédéric Dupuis]

As for order_dual, my experience with it has been that it's a great way to get one-line proofs, for example see all the lemmas about concave_on in analysis/convex/basic.

[Frédéric Dupuis]

But when one has to convert back and forth all the time between a type and its synonym it's quite painful.

[Damiano Testa]

Dear All,

I have been struggling to use the new version of monotone, using order_dual and I am ready to give up! I find it incredibly difficult to even understand if max' is using the "natural order" or the order_dual. In proofs, I constantly face goals of the form a=a where a : ℕ and a : order_dual ℕ. Almost never I am able to get Lean to realize that they are the same, since then rw, simp_rw, congr, convert ... all appear to fail.

It would be nice to have orders and their duals to work, but I am unable to understand how. In particular, I no longer know how to prove that nat_degree (reverse f) equals nat_degree f - nat_trailing_degree f.

If someone is willing to give it a try, I would be happy to see this method succeed! Otherwise, I would prefer to go back to the clunky-but-workable strategy of not introducing order_dual and instead using max and min on the same order.

[Johan Commelin]

Thanks a lot for trying. And I'm sorry to hear that the experiment failed.

[Johan Commelin]

Would you mind posting the file with your experiment?

[Damiano Testa]

sure, I will clean up the junk and produce a template to try out!

[Johan Commelin]

Merci!

[Damiano Testa]

you should be able to find the file here:

https://gist.github.com/adomani/6f82a36069e60b318741bdf8d3bcbf76

The file is quite long, but everything up to line 290 is essentially already in mathlib. My first change has been on line 291, with the introduction of order_dual and to_dual. After that, it has been a lot of pain to make progress. Lemma typ on line 349 is an extracted goal to see if things work out: you can safely ignore it! However, those are the kind of issues that sometimes I was able to overcome, but often stumped me!

Do ask questions: I am more than happy to learn from them!

[Damiano Testa]

I suspect that things might be easier if reverse and reflect were also defined using order_dual, but I am not sure that this would really be an improvement: I find it very hard to "switch on and off" order instances in Lean.

[Eric Wieser]

I'm confused - isn't to_dual already in mathlib? If so, why do you redefine it in your gist?

[Damiano Testa]

It is already in mathlib, but since not all the statements that follow are in mathlib, I included all that I knew was needed in order to produce a working (highly non-minimal) example!

[Damiano Testa]

(You will find other definitions and lemmas that are already in mathlib, but if you use this file with its imports, it seems to compile with no problems on my version of lean, up to line 360. In fact, up to 366, but I am not sure that my attempt really leads in a good direction.)

[Johan Commelin]

I just found out that we have strict_mono_decr_on in mathlib.
It seems really weird that we have that specific special case, but not mono_decr or strict_mono_decr in general.

[Johan Commelin]

I think that we are coming to the conclusion that order_dual is useful, but doesn't scale as a solution.

[Johan Commelin]

I'm starting to lean (no pun) towards the position that we should refactor to have separate notions of mono_incr and mono_decr with solid APIs for both of them. (One can be defined using order_dual, in terms of the other. I don't care.)

[Damiano Testa]

After a conversation with @Kevin Buzzard in this thread, I think that the suggestion was to prove a bunch of results with a "flabby" order_dual, so as to have a solid API. Eventually, though, making order_dual irreducible (something that I do not understand, so this might be nonsense) should give a workable setup.

To be honest, I am not entirely sure how this would work. For instance, I am very happy to have both min and max defined on ℕ and I would rather not have to switch to order_dual twice to convert a min to a max or vice-versa.

Also, if I have been following the various "galois connection" discussions, I suspect that this might be one, right?

[Kevin Buzzard]

Galois connections are all covariant in Lean! So in particular none of the ones I knew about before coming here (subsets of $\mathbb{A}^n$ and subsets of $k[X_1,\ldots,X_n]$, and, erm, Galois theory) are in Lean :-)

[Kevin Buzzard]

The ones in Lean right now are things like subsets of a group and subgroups of a group

[Damiano Testa]

Ahhhh!!! It had not clicked in me the issue with covariance/contravariance! In my mind, affine schemes "were essentially" in Lean, since there is a lot of commutative algebra!! Now that I had so much trouble getting results about leading coefficients imply results on trailing coefficients, I appreciate better the chasm that still exists!

[Damiano Testa]

Now that I am slightly more Lean-versed, I have a question.

When using the same type with different relations, I can see that this might cause confusion and introducing a type-synonym might make things worse: having two types for the natural numbers, one called ℕ and the other called order_dual ℕ is not so useful when you want to talk about max and min simultaneously.

However, when the relations are on "really" different types, like homomorphisms of comm_rings and morphisms of affine schemes, why is it a problem to set up the relations at the beginning, so that they match?

In the specific case of Galois theory, I might even go further and say that in Lean it might therefore be simpler to establish the Galois connection between subgroups and spectra of fields!!

[Kevin Buzzard]

Galois connection: that's an interesting idea :-) The issue with contravariant Galois connections is literally that the definition is not there.

[Damiano Testa]

Still, I am not sure that I understand this issue with covariance/contravariance too well. (The discussion below is likely a rambling based on a misconception.)

"In set theory", by construction, given any two mathematical objects A and B, they are sets and at least the question "is A a subset of B makes sense. Thus, the proper class of all mathematical objects is a poset (!). This is then abused and moved around identifications, but everyone always has a lingering feeling of what "containment" means, at least in local contexts. For instance, subgroups of Galois group are ordered by inclusion, fields are ordered by inclusion, these two natural orders, clash.

However, "in type theory", the poset structure needs to be provided externally. So, what is the problem with covariance/contravariance, if we get to choose which way the arrows point?

[Kevin Buzzard]

The computer scientists are always scared about the way things scale, at least this is my impression. If we define contravariant Galois connections then we have to define contravariant poset maps (a <= b -> f(a) >= f(b)) etc etc, and they say "we can just use order_dual and that's only one function so it scales". But it also makes things more complicated.

[Damiano Testa]

Ok, but then whichever one of min or max you define first, already implies the other, right?

[Damiano Testa]

(I am trying to undestand the basic principles, I am not trying to be snappy, in case the chat gives a wrong impression!)

[Kevin Buzzard]

min and max are still both defined on one type, they didn't go that far :-)

[Damiano Testa]

Would it then be the case that there should be an "orderless" bijection between ℕ and order_dual ℕ?

[Kevin Buzzard]

Sure, and that map should even have a name. If order_dual is semireducible then people might even use id for that name, but if it's irreducible then it would have an explicit name like to_dual or whatever.

[Damiano Testa]

Kevin Buzzard said:

min and max are still both defined on one type, they didn't go that far :-)

To be fair, I think that this is the right choice! But then, I would like to be able to say that a linear function is monotone increasing/decreasing, rather than having to define it from the correctly ordered type so that it is always monotone increasing!

[Kevin Buzzard]

I guess some people are defining antimono functions, but we don't have contravariant Galois connections or insertions yet, like we don't have functions from A to B such that $f(xy)=f(x)+f(y)$. People look at definitions like this and are scared that such a definition will lead to some chaos, but I'm not convinced it will. Another example is contravariant functors. You have to decide which category to put the "op" on and there is no canonical answer. Another way of doing it would just to have been to define contravariant_functor to be a map between the categories and write down the axioms rather than opping something. The disadvantage with this approach is that then there's a risk you have to develop the entire functor API again in the contravariant setting. Perhaps a solution to this would be to write a tactic using a @[to_contravariant] tag, but this would be hard work.

[Damiano Testa]

It is a little frustrating that the innocent-looking assertion "reverse all the arrows in your category" causes so much trouble in formalization

[Damiano Testa]

However, even the consequences for intuition of such a change are huge: no one had realized that commutative rings with 1 are affine schemes, until Grothendieck, I think!

[Kevin Buzzard]

Think about it this way. Is a contravariant functor actually equal to (a) a covariant functor $C\to D^{op}$ (b) a covariant functor $C^{op}\to D$ (c) a map $C\to D$ with some properties? All of these are "the same" but in fact none of them are the same. Machinery should be able to cover this up, whether it's a good API or good tactics, but this machinery needs to be made.

[Damiano Testa]

I agree: I personally like to have the opposite and place it on the category that I am less familiar with! I can see how this is somewhat difficult to formalize... :grinning:

[Joseph Myers]

There's a galois_connection using order_dual in analysis.normed_space.inner_product for orthogonal complements of subspaces. (Immediately followed by a series of lemmas with one-line proofs, so that you don't need to think about two different orders on subspaces at the same time in order to use those properties of orthogonal subspaces.)