Caratheodory

Stream: maths

[Johan Commelin]

I fixed some of the easier sorrys on caratheodory2 and enabled bigops notation.

[Johan Commelin]

Removed another one

[Johan Commelin]

convex_coefficients is now sorry free

[Scott Morrison]

Excellent. exists_nontrivial_relation_of_dim_lt_card is now sorry free.

[Scott Morrison]

There's one piece of maths still to do:

lemma exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card
  {t : finset E} (h : findim ℝ E + 1 < t.card) :
  ∃ f : E → ℝ, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0 :=
begin
  -- pick an element x₀ ∈ t,
  -- apply the previous lemma to the other xᵢ - x₀,
  -- to obtain a function `f`
  -- and then adjust f x₀ := - others.sum f
  sorry
end

and five easy sorries in mem_convex_hull_erase.

[Johan Commelin]

five - four = one

[Johan Commelin]

@Scott Morrison are you working on this atm?

[Scott Morrison]

I'd just paused for a bit, but yes, apparently we've been working at the same time.

[Johan Commelin]

Only 1 sorry left! (@Scott Morrison)

[Scott Morrison]

Just merged our changes.

[Scott Morrison]

It's surprisingly unpainful to have two people working at once

[Johan Commelin]

Well, we weren't doing the same lemma

[Johan Commelin]

That would have been painful, I guess

[Johan Commelin]

@Scott Morrison why is the final sorry true?

[Scott Morrison]

it seems I have to do some recompiling

[Scott Morrison]

I guess that is a downside of too-active work on a branch :-)

[Mario Carneiro]

Johan Commelin said:

five - four = one

have you tried by norm_num?

[Johan Commelin]

@Scott Morrison I found my way out

[Johan Commelin]

@Mario Carneiro Can norm_num already count sorrys in a file?

[Scott Morrison]

I'm wondering if we should ship this branch to the sphere-eversion repository, postponing putting it in mathlib.

[Mario Carneiro]

no, but it can verify exactly how far from done you are :)

[Johan Commelin]

@Scott Morrison @Patrick Massot We're sorry free

[Scott Morrison]

I want to tack on a final theorem

[Scott Morrison]

given an explicit centre-of-mass of (d+1)-points formula

[Johan Commelin]

Go ahead. I need to prepare an exercise sheet :head_bandage:

[Scott Morrison]

it's essentially just unfolding a definition

[Patrick Massot]

Why do you want postponing putting it in mathlib?

[Patrick Massot]

There are a lot of specialized lemmas in this project, but that one goes to mathlib without any discussion.

[Patrick Massot]

I mean we can discuss the implementation, but not the fact it belongs to mathlib.

[Johan Commelin]

I would like to keep the number of lines in the sphere eversion project ≤ 2 as long as possible :grinning_face_with_smiling_eyes:

[Scott Morrison]

I do want to make a PR to sphere-eversion to learn how to make something have a green background in the dependency graph. :-)

[Scott Morrison]

Presumably we should also make a PR to sphere-eversion to provide a link to the theorem once it is merged into mathlib.

[Scott Morrison]

Should we in the meantime give a link to the PR or something?

[Jalex Stark]

If the point of the dependency graph is to track sorries, then we should color caratheodory on the dependency graph as soon as there's a PR to mathlib which has no sorries and provides the theorem.

[Jalex Stark]

a low-tech and probably-bad way to do this is to copy-paste the proof from the PR, and leave a note saying "once mathlib#xxxx is merged, we can replace all of the proofs in these files with calls to the library"

[Jalex Stark]

a higher-tech thing would be to have a sphere-eversion branch of mathlib, and have it accept a merge from caratheodory2 as soon as it's sorry free

[Jalex Stark]

then the post-game work after defeating sphere-eversion is clear : get the sphere-eversion branch merged into master. this requires getting all of the machinery that was written as mathlib PRs to get merged into master.

[Johan Commelin]

I suggest adding an extra color or badge to differentiate between sorry-free and merged-into-mathlib.

[Johan Commelin]

Because both are interesting states, but there can still be a decent amount of work between sorry-free and merge-into-mathlib.

[Jalex Stark]

oh i guess we expect everything to end up in mathlib, and there are parts that we're PRing to mathlib early because they live far away from differential_topology or wherever the bulk of this work is going to end up

[Patrick Massot]

If we want everything into mathlib then the mathlib badge is not being in the project repo

[Johan Commelin]

But it would be nice to see this in the graph

[Patrick Massot]

Maybe a lighter green for stuff not in mathlib then?

[Johan Commelin]

sounds good

[Patrick Massot]

Let me officially start to change the blueprint because it was not precise enough. This is related to Scott's comment. So we no longer have Carathédory's lemma, because I slightly strengthened the statement. The good point is that the next lemma now has a proof blueprint.

[Patrick Massot]

I'd like to also write a proof blueprint for Carathéodory, but I fear it wouldn't match the almost proof that is currently PRed, so I'll let other people do that.

[Scott Morrison]

Should we have stacks-style tags for statements in the blue print?

[Scott Morrison]

(i.e. names that don't change when theorem numbering changes?

[Scott Morrison]

It might be helpful when development is happening directly in mathlib or elsewhere on a "blueprinted" goal, to be able to give stable references back to the motivating points of a blueprint.

[Yury G. Kudryashov]

Do you mean LaTeX-style labels?

[Yury G. Kudryashov]

Can't we use implicit function theorem to get Lemma 1.6 for free?

[Yury G. Kudryashov]

No, we still need the derivative of center_mass w.r.t. the weights.

[Scott Morrison]

@Yury G. Kudryashov. Yes. More specifically, the suggestion was the the LaTeX style labels are just opaque alphanumeric identifiers, but with the implicit promise that they will never change. (If the theorem statement itself needs to change significantly, it should be given a new label.)

[Yury G. Kudryashov]

But the link https://leanprover-community.github.io/sphere-eversion/blueprint/chap-loops.html#lem:smooth_convex_hull contains the LaTeX label. What else do you want?

[Scott Morrison]

1. To know how to name the corresponding Lean file for that lemma.
2. To know how to refer to that lemma from a PR to mathlib
3. To know what string to search for to find existing work on this lemma in the sphere-eversion repository.

lem:smooth_convex_hull doesn't quite answer all of these questions, because it's not a valid file name. But I agree it's close.
Including chap-loops.html in the unique identifier seems dangerous, because then it Patrick ever wants to move files around links break.

[Scott Morrison]

The Stacks Project solution is described at https://stacks.math.columbia.edu/tags

[Scott Morrison]

(deleted)

[Scott Morrison]

@Patrick Massot, I think I disagree with your decision to strengthen the statement of Caratheodory's convexity itself in your blueprint.

1. It makes it different from the statements I can find in the literature (which don't bother saying the coefficients are nonzero), and indeed more complicated.
2. It's very easy to prove from the usual statement: "Finally discard any of the points with coefficient zero."
3. It just seems more natural to postpone talking about positive coefficients at all until we're in a context where it matters: we add the assumption the original set is open.

[Scott Morrison]

In any case, I pushed to caratheodory2 an incomplete proof of the statement including positivity.

[Scott Morrison]

Still a little big_operator munging to do; two sorries remain.

[Patrick Massot]

Sorry I'm late to this discussion, I've been on family duty all day. I just started my computer 10 minutes ago.

[Patrick Massot]

About the TeX label vs identifier discussion, I don't think we need to go down the stacks tag road. The Stacks project is about 6000 pages of mathematics which evolved a lot, and is cited in a lot of papers. Here we are discussing formalizing 20 pages of mathematics, even if I suspect it will be at least 30 pages at the end of the project. TeX labels are unique within a TeX document, and they can carry information. Certainly my choice of labels could be improved, but they are meant to help reading the dependency graph.

[Patrick Massot]

Of course I want to automatically generate links to the source code from the website, instead of hardcoding them in the TeX source as is currently done. I'll work on that really soon. I didn't think about it but we could also have special comments in the Lean source referring to tex labels, and CI could check that those labels exist in the TeX source. This is all easy to do, it only takes time.

[Patrick Massot]

About Carathéodory, I hesitated and went for the lazy solution, but I agree that we should stick to the usual statement for the lemma that is called Carathéodory in the TeX and Lean, and state the slightly more precise corollary as another lemma.

[Patrick Massot]

Yury G. Kudryashov said:

Can't we use implicit function theorem to get Lemma 1.6 for free?

If you look at the git history, you'll see this was the original plan. But somehow I had remorse yesterday because this implicit function is totally explicit. Actually the current version of the proof is not totally explicit because I needed to go to bed, but I'll finish expliciting it tonight. I'm not too happy about how long it turned out to be in TeX, so I wouldn't mind going back to the implicit function plan. In terms of library development I think both roads are interesting. Making sure the implicit function theorem is nice to use is important, and developing linear algebra is important. For instance the elementary road I have in mind would use the determinant of a family of vectors with respect to a basis, and I think we don't have that yet.

[Patrick Massot]

I pushed details about smoothness of the explicit function in https://github.com/leanprover-community/sphere-eversion/commit/e64b710025e18c7432b86775d714ef8b96f21aa5

[Johan Commelin]

I created #3030 (@Scott Morrison) that splits of all the smaller changes (10 files, ~138 lines).
What remains is 2 larger diffs.

[Patrick Massot]

I lost track of the plan here. Are we still waiting for some affine geometry stuff? Or are you trying to get the linear space version merged?

[Scott Morrison]

I think it makes sense to merge the vector space version, and to plan to upgrade it to affine spaces later, when the requirements are in place, and someone has the energy/need.

"Perfect is the enemy of good."

[Floris van Doorn]

(deleted)

[Johan Commelin]

We now have a version of Carathéodory in mathlib ( :tada:) but I think this was no longer exactly the statement that was needed for Sphere Eversion, right?

[Patrick Massot]

I'll switch back to this statement in the sphere eversion project, and add the more precise statement as another lemma.

[Johan Commelin]

Does that mean we get some green in the graph? :green_heart:

[Patrick Massot]

Yes, I'll try to do that tonight

[Johan Commelin]

Awesome!

[Patrick Massot]

I'm confused now. I wanted to update the sphere eversion but #2960 actually isn't merged, right?

[Bryan Gin-ge Chen]

@Patrick Massot Do you mind giving your approval to bors if you're happy with it?

[Johan Commelin]

Huh... I don't know why I thought so.... but I was convinced it was merged.

[Patrick Massot]

Carathéodory now appears in green at https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph.html. But the proof probably needs refactoring in order to prove the refined statement. Note that https://github.com/leanprover-community/mathlib/blob/a432a3a193aac390d347835881f48a5e5bac6ed9/src/analysis/convex/caratheodory.lean#L213 is only half of the refinement (dropping the points having vanishing weights, but without ensuring the remaining points are affinely independent).

[Patrick Massot]

Also, that lemma didn't have a proof in the blueprint, so I added one following the Lean code. It's hard to believe that the Lean proof wouldn't be simpler by using a map from fin n to E instead of a finset E. I couldn't bring myself to use weights indexed by points of E in the blueprint.

[Yaël Dillies]

@Oliver Nash, what do you think are the correct assumptions on the base monoid in Carathéodory? It's currently ℝ because convexity is only defined in real vector spaces, but I'm changing that.

[Oliver Nash]

Good question; maybe linear_ordered_field?

[Yaël Dillies]

Yeah, you seem to use division. I was wondering this could be relaxed to ordered_comm_ring

[Oliver Nash]

I think that as stated, division is necessary. Say the coefficients are k, we have a set t of n points whose convex hull contains the input point x, and which we want to prove are affine independent. The proof works in k^n by starting with a point in the simplex of coefficients whose affine span against t gives x. The argument is then that if t is not affinely indepdendent, there is a line in this simplex giving a full line of coefficients whose affine span against t gives x. But this line must intersect a side (in fact two sides I guess) of the simplex so we can reduce the cardinality (which is a contradiction if n was chosen to be minimal).

[Oliver Nash]

To do that intersection, I think you'll need division.

[Yaël Dillies]

And do we have any weaker division ordered typeclass?

[Oliver Nash]

I don't think so but I'd be happy to be proved wrong. In my head the only semiring that is simultaneously ordered, commutative, has negatives, has division is linear_ordered_field.

[Scott Morrison]

You don't want to do non-commutative convex spaces? :-)

[Yaël Dillies]

Eheh, that will be the new generality for most stuff in analysis.convex.basic :sweat_smile:

[Oliver Nash]

Come to think of it, I don't know any examples of non-commutative linearly-ordered rings. Do they exist?

[Scott Morrison]

https://math.stackexchange.com/questions/621111/existence-of-non-commutative-ordered-ring

[Yaël Dillies]

Yeah of course.

[Kevin Buzzard]

I'm not sure this construction is so obvious!

[Yaël Dillies]

No, the construction is absolutely non-obvious! But there's not strong incentive for linearity to imply commutativity.

[Oliver Nash]

Sometimes weird things are true though. Eg., Wedderburn's little theorem

[Yaël Dillies]

Yeah, I guess!

[Julian Külshammer]

Lam's books are a great source for examples.

[Yaël Dillies]

To continue the discussion, do nonlinear ordered fields exist?

[Kevin Buzzard]

You mean a partially ordered field? What are the axioms? How about any field with a<=b iff a=b?

[Yaël Dillies]

Take ordered_comm_ring and add division with hypothesis that it is monotone/strict_mono for positive elements.

[Reid Barton]

I was going to give a less trivial example like: $\mathbb{Q}(\sqrt{2})$ has two orders; so if we take their intersection then we get a new partial order

[Reid Barton]

That's a partially ordered ring (ordered_comm_ring) which is also a field, if I'm not mistaken.

[Reid Barton]

AFAIK, the phrase "ordered field" always means linearly ordered.

[Yaël Dillies]

Yeah, I ask because we go straigh from ordered_comm_ring to linear_ordered_field.

[Reid Barton]

It seems to me there is linear_ordered_comm_ring in between.

[Reid Barton]

(btw, these names ought to be linearly_ordered_*)

[Yaël Dillies]

I meant on the nonlinear part. I was expecting ordered_field to exist.

[Reid Barton]

I think it's not really an important notion. The example of $\mathbb{Q}(\sqrt{2})$ with the weird partial order is a partially ordered ring, but in that context it doesn't deserve to be called a "field" because it has two incompatible maps to ordered fields (in one of them $\sqrt{2}$ goes to something positive, in the other one something negative).

[Reid Barton]

I would say having ordered_field with the definition "partially ordered ring that's a field" would be confusing.

[Reid Barton]

e.g. the nLab says "Note that while the adjective ‘ordered’ usually refers to a partial order, it is traditionally used more strictly when placed before ‘field’."

[Kevin Buzzard]

Reid's example is better than mine because I think 0<1 is a nice property

[Yaël Dillies]

I think this tells more about $\mathbb Q(\sqrt 2)$ than about the concept of ordered field.

[Reid Barton]

Right, in a sense it's the same thing that happened already for rings. A partially ordered ring isn't a partially ordered set that's also a ring. There is some compatibility. For a field, the right compatibility is apparently that the partial order is actually a total order.
I reailze now you mentioned division--division is sort of a funny thing, but I think any reasonable axiom about division preserving order will be satisfied by the funny $\mathbb{Q}(\sqrt{2})$ because it is satisfied in both of the total orders.

[Yaël Dillies]

Hmm... I am still not convinced ordered_field isn't something we should have.

[Reid Barton]

The bigger picture is that in algebraic geometry a field looks like a point, while in real algebraic geometry (which is actually about ordered rings and has little to do with the real numbers specifically) $\mathbb{Q}(\sqrt{2})$ looks like two points.

[Yaël Dillies]

And would that be true of any reasonable nonlinear ordered field we come up with?

[Reid Barton]

Well mathlib has a lot of type classes already that don't have any particular use in math (distrib?). But if we do have such a class it shouldn't be called ordered_field even if that's consistent with the other names, because that's not what "ordered field" means.

[Yaël Dillies]

Uh? I don't get your point here.

[Reid Barton]

I mean we should definitely not have class ordered_field whose definition is just the combination of ordered_comm_ring and field

[Reid Barton]

but it could be called partially_ordered_field or something like that

[Yaël Dillies]

Yes of course. I mean to assume monotonicity of division in the same way linear_ordered_field does.

[Reid Barton]

Sorry, I should have said that if there is a class ordered_field, then it must have the usual mathematical meaning (linearly ordered field).

[Yaël Dillies]

I'm coming to that from "I don't actually use linearity of my field very often. Why is it even in the typeclass?"

[Johan Commelin]

In the $\mathbb Q(\sqrt 2)$ example, the elements that are positive in both orders are called "totally positive elements". These things show up in CM theory of abelian varieties. Where "totally real number fields" play a role: they are the finite extensions of $\mathbb Q$ for which every embedding in $$\mathbb C$ lands in $\R$.

[Yaël Dillies]

Interesting, interesting. And those are ordered field which in general aren't ordered, right?

[Reid Barton]

There is also the example of $\mathbb{C}$ with the partial order "$a \le b$ if $b - a$ is real and nonnegative" which has been discussed here before

[Yaël Dillies]

Does that make it into an ordered anything?

[Yaël Dillies]

ordered_add_comm_monoid, surely, but what happens with multiplication?

[Reid Barton]

It's a partially ordered ring with monotone division, because the only "positive" elements are the positive reals

[Yaël Dillies]

Oooh, yes I see

[Reid Barton]

this example is a bit different because $\mathbb{C}$ doesn't have any linear orders (because $-1$ is a square)

[Kevin Buzzard]

Yaël Dillies said:

Interesting, interesting. And those are ordered field which in general aren't ordered, right?

When dealing with totally positive elements of a number field one does not talk about the partial ordering (which as far as I know is not at all useful). One reason totally positive elements are useful is that there's a concept of a CM field, which is a totally imaginary extension of a totally real field, and which is obtained by adjoining a square root of a totally positive element. However I would envisage, when we get this far, just having a predicate is_totally_positive on elements of a number field, as opposed to using the partial order and then continually referring to the elements which are > 0 for this order: the point is that you don't ever talk about a < b in general, it's just this specific predicate which turns out to be useful.

[Yaël Dillies]

And what does CM stand for?

[Kevin Buzzard]

Complex Multiplication, it's some technical term coming from the theory of abelian varieties

[Kevin Buzzard]

Given a general lattice L (discrete subgroup isomorphic to Z^2) in the complex numbers, like \Z+\Z*tau for some random complex non-real number tau, the set of complex numbers z such that z*L is a subset of L is usually just the integers, but for some special lattices you can get non-integer values of z which work -- for example if L=Z[i] then any z in Z[i] works. We say the associated elliptic curve C/L has complex multiplication. For higher dimensional complex tori more general CM fields come into play. The basic theory is surprisingly delicate but has been well-understood since the 1940s or so.

[Johan Commelin]

Kevin Buzzard said:

there's a concept of a CM field, which is a totally imaginary extension of a totally real field, and which is obtained by adjoining a square root of a totally positive element.

I think you adjoin a square root of a totally negative element. But that's not too relevant for this discussion.

[Kevin Buzzard]

Thanks -- fixed