Zulip Chat Archive

Stream: maths

Topic: Caratheodory


Johan Commelin (Jun 04 2020 at 19:36):

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

Johan Commelin (Jun 04 2020 at 20:07):

Removed another one

Johan Commelin (Jun 04 2020 at 20:13):

convex_coefficients is now sorry free

Scott Morrison (Jun 05 2020 at 02:30):

Excellent. exists_nontrivial_relation_of_dim_lt_card is now sorry free.

Scott Morrison (Jun 05 2020 at 02:30):

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 (Jun 05 2020 at 09:09):

five - four = one

Johan Commelin (Jun 05 2020 at 09:16):

@Scott Morrison are you working on this atm?

Scott Morrison (Jun 05 2020 at 09:30):

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

Johan Commelin (Jun 05 2020 at 09:31):

Only 1 sorry left! (@Scott Morrison)

Scott Morrison (Jun 05 2020 at 09:31):

Just merged our changes.

Scott Morrison (Jun 05 2020 at 09:31):

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

Johan Commelin (Jun 05 2020 at 09:32):

Well, we weren't doing the same lemma

Johan Commelin (Jun 05 2020 at 09:32):

That would have been painful, I guess

Johan Commelin (Jun 05 2020 at 09:33):

@Scott Morrison why is the final sorry true?

Scott Morrison (Jun 05 2020 at 09:35):

it seems I have to do some recompiling

Scott Morrison (Jun 05 2020 at 09:35):

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

Mario Carneiro (Jun 05 2020 at 09:38):

Johan Commelin said:

five - four = one

have you tried by norm_num?

Johan Commelin (Jun 05 2020 at 09:38):

@Scott Morrison I found my way out

Johan Commelin (Jun 05 2020 at 09:39):

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

Scott Morrison (Jun 05 2020 at 09:40):

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

Mario Carneiro (Jun 05 2020 at 09:40):

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

Johan Commelin (Jun 05 2020 at 09:42):

@Scott Morrison @Patrick Massot We're sorry free

Scott Morrison (Jun 05 2020 at 09:42):

I want to tack on a final theorem

Scott Morrison (Jun 05 2020 at 09:42):

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

Johan Commelin (Jun 05 2020 at 09:42):

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

Scott Morrison (Jun 05 2020 at 09:42):

it's essentially just unfolding a definition

Patrick Massot (Jun 05 2020 at 09:44):

Why do you want postponing putting it in mathlib?

Patrick Massot (Jun 05 2020 at 09:44):

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

Patrick Massot (Jun 05 2020 at 09:45):

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

Johan Commelin (Jun 05 2020 at 09:46):

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 (Jun 05 2020 at 10:16):

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 (Jun 05 2020 at 10:16):

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 (Jun 05 2020 at 10:17):

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

Jalex Stark (Jun 05 2020 at 19:15):

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 (Jun 05 2020 at 19:16):

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 (Jun 05 2020 at 19:18):

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 (Jun 05 2020 at 19:21):

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 (Jun 05 2020 at 19:30):

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

Johan Commelin (Jun 05 2020 at 19:31):

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

Jalex Stark (Jun 05 2020 at 19:34):

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 (Jun 05 2020 at 19:36):

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

Johan Commelin (Jun 05 2020 at 19:37):

But it would be nice to see this in the graph

Patrick Massot (Jun 05 2020 at 19:38):

Maybe a lighter green for stuff not in mathlib then?

Johan Commelin (Jun 05 2020 at 19:46):

sounds good

Patrick Massot (Jun 06 2020 at 13:21):

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 (Jun 06 2020 at 13:23):

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 (Jun 07 2020 at 02:49):

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

Scott Morrison (Jun 07 2020 at 02:49):

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

Scott Morrison (Jun 07 2020 at 02:50):

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 (Jun 07 2020 at 03:47):

Do you mean LaTeX-style labels?

Yury G. Kudryashov (Jun 07 2020 at 04:06):

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

Yury G. Kudryashov (Jun 07 2020 at 04:17):

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

Scott Morrison (Jun 07 2020 at 04:19):

@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 (Jun 07 2020 at 04:21):

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 (Jun 07 2020 at 04:28):

  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 (Jun 07 2020 at 04:29):

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

Scott Morrison (Jun 07 2020 at 04:34):

(deleted)

Scott Morrison (Jun 07 2020 at 04:43):

@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 (Jun 07 2020 at 05:01):

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

Scott Morrison (Jun 07 2020 at 05:01):

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

Patrick Massot (Jun 07 2020 at 17:25):

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 (Jun 07 2020 at 17:28):

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 (Jun 07 2020 at 17:31):

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 (Jun 07 2020 at 17:33):

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 (Jun 07 2020 at 17:38):

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 (Jun 07 2020 at 21:46):

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

Johan Commelin (Jun 11 2020 at 13:58):

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

Patrick Massot (Jun 11 2020 at 20:29):

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 (Jun 11 2020 at 23:40):

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 (Jun 12 2020 at 04:12):

(deleted)

Johan Commelin (Jun 15 2020 at 16:55):

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 (Jun 15 2020 at 17:52):

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

Johan Commelin (Jun 15 2020 at 17:53):

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

Patrick Massot (Jun 15 2020 at 17:54):

Yes, I'll try to do that tonight

Johan Commelin (Jun 15 2020 at 17:54):

Awesome!

Patrick Massot (Jun 15 2020 at 21:19):

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

Bryan Gin-ge Chen (Jun 16 2020 at 03:19):

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

Johan Commelin (Jun 16 2020 at 04:58):

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

Patrick Massot (Jun 16 2020 at 20:00):

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 (Jun 16 2020 at 20:02):

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 (Sep 07 2021 at 07:00):

@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 (Sep 07 2021 at 07:02):

Good question; maybe linear_ordered_field?

Yaël Dillies (Sep 07 2021 at 07:11):

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

Oliver Nash (Sep 07 2021 at 07:22):

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 (Sep 07 2021 at 07:22):

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

Yaël Dillies (Sep 07 2021 at 07:32):

And do we have any weaker division ordered typeclass?

Oliver Nash (Sep 07 2021 at 07:37):

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 (Sep 07 2021 at 09:08):

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

Yaël Dillies (Sep 07 2021 at 10:15):

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

Oliver Nash (Sep 07 2021 at 10:15):

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

Scott Morrison (Sep 07 2021 at 10:16):

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

Yaël Dillies (Sep 07 2021 at 10:16):

Yeah of course.

Kevin Buzzard (Sep 07 2021 at 10:17):

I'm not sure this construction is so obvious!

Yaël Dillies (Sep 07 2021 at 10:18):

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

Oliver Nash (Sep 07 2021 at 10:19):

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

Yaël Dillies (Sep 07 2021 at 10:20):

Yeah, I guess!

Julian Külshammer (Sep 07 2021 at 19:17):

Lam's books are a great source for examples.

Yaël Dillies (Sep 11 2021 at 09:46):

To continue the discussion, do nonlinear ordered fields exist?

Kevin Buzzard (Sep 11 2021 at 10:09):

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

Yaël Dillies (Sep 11 2021 at 10:12):

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

Reid Barton (Sep 11 2021 at 10:12):

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

Reid Barton (Sep 11 2021 at 10:14):

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

Reid Barton (Sep 11 2021 at 10:14):

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

Yaël Dillies (Sep 11 2021 at 10:15):

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

Reid Barton (Sep 11 2021 at 10:17):

It seems to me there is linear_ordered_comm_ring in between.

Reid Barton (Sep 11 2021 at 10:17):

(btw, these names ought to be linearly_ordered_*)

Yaël Dillies (Sep 11 2021 at 10:18):

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

Reid Barton (Sep 11 2021 at 10:39):

I think it's not really an important notion. The example of Q(2)\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 2\sqrt{2} goes to something positive, in the other one something negative).

Reid Barton (Sep 11 2021 at 10:40):

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

Reid Barton (Sep 11 2021 at 10:44):

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 (Sep 11 2021 at 10:49):

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

Yaël Dillies (Sep 11 2021 at 10:56):

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

Reid Barton (Sep 11 2021 at 10:56):

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 Q(2)\mathbb{Q}(\sqrt{2}) because it is satisfied in both of the total orders.

Yaël Dillies (Sep 11 2021 at 10:58):

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

Reid Barton (Sep 11 2021 at 11:00):

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) Q(2)\mathbb{Q}(\sqrt{2}) looks like two points.

Yaël Dillies (Sep 11 2021 at 11:02):

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

Reid Barton (Sep 11 2021 at 11:02):

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 (Sep 11 2021 at 11:03):

Uh? I don't get your point here.

Reid Barton (Sep 11 2021 at 11:04):

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

Reid Barton (Sep 11 2021 at 11:05):

but it could be called partially_ordered_field or something like that

Yaël Dillies (Sep 11 2021 at 11:05):

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

Reid Barton (Sep 11 2021 at 11:06):

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 (Sep 11 2021 at 11:06):

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 (Sep 11 2021 at 11:07):

In the Q(2)\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 Q\mathbb Q for which every embedding in $$\mathbb C$ lands in R\R.

Yaël Dillies (Sep 11 2021 at 11:09):

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

Reid Barton (Sep 11 2021 at 11:11):

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

Yaël Dillies (Sep 11 2021 at 11:12):

Does that make it into an ordered anything?

Yaël Dillies (Sep 11 2021 at 11:12):

ordered_add_comm_monoid, surely, but what happens with multiplication?

Reid Barton (Sep 11 2021 at 11:13):

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

Yaël Dillies (Sep 11 2021 at 11:13):

Oooh, yes I see

Reid Barton (Sep 11 2021 at 11:17):

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

Kevin Buzzard (Sep 11 2021 at 15:35):

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 (Sep 11 2021 at 17:35):

And what does CM stand for?

Kevin Buzzard (Sep 11 2021 at 17:35):

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

Kevin Buzzard (Sep 11 2021 at 17:38):

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 (Sep 11 2021 at 18:02):

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 (Sep 11 2021 at 18:02):

Thanks -- fixed


Last updated: Dec 20 2023 at 11:08 UTC