## 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

#### 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?

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

(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."

(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

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.

Last updated: May 09 2021 at 09:11 UTC