Zulip Chat Archive

Stream: maths

Topic: Sphere eversion project


view this post on Zulip Patrick Massot (Jun 03 2020 at 15:52):

Hi everybody! I'm very excited to announce the official start of the sphere eversion project! I mentioned this dream during FoMM2020 in Pittsburgh, but it has now started. You can read a first version of the blueprint, either in pdf or online, although the third chapter is currently pretty rough.

Everybody is welcome to contribute. There is plenty to do, as you can see from this graph (read the legend and click nodes). The first two chapters are completely elementary, and contain enough material for publication in CPP or ITP.

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 16:06):

I'm attempting Carathéodory's lemma :)

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:11):

That would be the second item to get its check-mark, after https://leanprover-community.github.io/sphere-eversion/blueprint/chap-local.html#def:ample_subset

view this post on Zulip Sebastien Gouezel (Jun 03 2020 at 16:12):

Is there a plan with respect to mathlib integration? I mean, PR early and PR often, or get something complete and polished and PR in the end?

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:15):

We already tried "PR in the end" in the perfectoid project... As you can see from the existence of a blueprint, I'm trying new stuff for this project.

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:16):

I don't understand the difference between "blue bg": proof ready, and "green bg": proof done.

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:16):

Proof ready to be formalized

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:16):

Aha

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:16):

As in: all dependencies are green?

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:16):

It means everything the proof depends on has been formalized.

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:17):

Yes

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:17):

Hopefully this is clear in the explanation on the project home page. This legend is already too long

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:18):

On the project homepage, I would add " for formalization" after the word "ready" (2x)

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:19):

PR!

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 16:20):

main motivations on web page: non-sense -> nonsense and pionneered -> pioneered

view this post on Zulip Sebastien Gouezel (Jun 03 2020 at 16:20):

Before formalizing loops, shouldn't one formalize the circle?

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:21):

I explain somewhere that a map on S1\mathbb S^1 is a periodic map on R\mathbb R.

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:22):

And we'll need that point of view anyway, in order to write down the key construction at https://leanprover-community.github.io/sphere-eversion/blueprint/chap-local.html#def:corrugation

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 16:24):

When can I do sep#corrugation?

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:25):

sphere#1

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 16:26):

That's a good start

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:26):

(@Sebastian Ullrich Here's your chance for another +5xp by making another zulip linkifier.)

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:28):

Sebastien Gouezel said:

Is there a plan with respect to mathlib integration? I mean, PR early and PR often, or get something complete and polished and PR in the end?

I suggest "PR early and often". (It shouldn't be hard to allow linking to lean facts in mathlib besides the sphere repo. Maybe it's already supported!)

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:34):

Kevin, corrugation probably need the integration PRs that are stuck in the queue since January.

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:35):

Sure we'll have links to mathlib. Currently the linking stuff is very primitive, see our only example at https://github.com/leanprover-community/sphere-eversion/blob/master/blueprint/src/local_convex_integration.tex#L290

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:36):

I see the possibility of shortening that url a bit (-;

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 16:36):

Maybe you should manually go through some levels and flag them as mathlib-candidates, and in your fancy interface you can flag what is not formalised, what is not proved, and what is not PR'ed.

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:37):

image.png

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:37):

This is what the website looks like on a small screen

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:38):

Would it be possible to devote only 25% width to the blue ToC?

view this post on Zulip Patrick Massot (Jun 03 2020 at 16:39):

Sure, but not today. Although we can overwrite this in the leanblueprint plasTeX plugin, this change could be made directly to the default CSS of plasTeX.

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:55):

sphere#2

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:41):

Bhavik Mehta said:

I'm attempting Carathéodory's lemma :)

If anyone feels like joining in, I'm streaming this in the Xena discord - going pretty slowly so far

view this post on Zulip Johan Commelin (Jun 03 2020 at 18:41):

@Bhavik Mehta were you working on a mathlib branch?

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:41):

No

view this post on Zulip James Arthur (Jun 03 2020 at 19:17):

A slightly out of the blue question but as a spir of this could you prove hairy ball theorem with all the Maths here?

view this post on Zulip Patrick Massot (Jun 03 2020 at 19:55):

There is some intersection of tool sets but not much. But the hairy ball theorem is quite a bit easier.

view this post on Zulip Scott Morrison (Jun 03 2020 at 23:18):

regarding mathlib integration, could I suggest the (fantastic!) dependency graph page uses three colours, to indicate:

  • "Ready for formalisation"
  • "Draft version ready" (i.e. in the sphere-eversion repository)
  • "Complete" (i.e. in mathlib)

view this post on Zulip Scott Morrison (Jun 03 2020 at 23:18):

(This would implicitly set expectations that we need to get stuff PR'd.)

view this post on Zulip Scott Morrison (Jun 04 2020 at 02:01):

@Bhavik Mehta I couldn't find any trace of what you did on discord earlier, so perhaps this was duplicative, but I just PR'd what is hopefully a helpful step to Caratheodory's lemma. #2944.

view this post on Zulip Bhavik Mehta (Jun 04 2020 at 02:02):

Thanks - I didn't end up making much progress, was mostly trying to figure out how the dimension API works

view this post on Zulip Bhavik Mehta (Jun 04 2020 at 02:14):

I think the main things that would be helpful right now is the stuff mentioned here

view this post on Zulip Scott Morrison (Jun 04 2020 at 02:48):

An alternative would be to have some sort of "badge" that could be attached to each ellipse or rectangle that indicated that it was in now in mathlib.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:01):

I pushed a simpler proof of #2944. Now I think that I should review it. Let's wait for @Patrick Massot or @Sebastien Gouezel .

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:03):

Scott Morrison said:

I couldn't find any trace of what you did on discord earlier

What exactly means "on discord" here? I just wonder if I need +1 account/open tab to know what happens.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:06):

BTW, I don't understand why do you need this for Carathéodory.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:07):

You can start with rw [convex_hull_eq], rcases, then deal with a finset with indexes in ι.

view this post on Zulip Scott Morrison (Jun 04 2020 at 04:08):

It's certainly not strictly necessary. I was going to take a point in the convex hull, use this lemma to see it is in the convex hull of some finset, and then reduce the cardinality of that finset in steps.

view this post on Zulip Scott Morrison (Jun 04 2020 at 04:10):

What exactly means "on discord" here? I just wonder if I need +1 account/open tab to know what happens.

Kevin has a discord server for talking to students at Imperial. Bhavik mentioned that he was working on caratheodory in a livestream there, so I went looking for it. I'd never been there before today.

view this post on Zulip Scott Morrison (Jun 04 2020 at 04:12):

@Yury G. Kudryashov, what statement did you have in mind for Carathéodory? I was thinking about

lemma caratheodory (s : set E) :
  convex_hull s =  (t : finset E) (w : t  s) (b : t.card  findim  E + 1), convex_hull t :=

view this post on Zulip Scott Morrison (Jun 04 2020 at 04:12):

which hence lead me away from using indices.

view this post on Zulip Scott Morrison (Jun 04 2020 at 04:17):

(And then proving this from

lemma caratheodory_reduction (t : finset E) (h : findim  E + 1 < t.card) :
  convex_hull (t : set E) =  (x : (t : set E)), convex_hull (t.erase x) :=
sorry -- this is the real work

lemma caratheodory_reduction' (t : finset E) :
  convex_hull (t : set E) =
     (t' : finset E) (w : t'  t) (b : t'.card  findim  E + 1), convex_hull t' :=
sorry -- just an induction and playing with sets

and the lemma in #2944.)

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:17):

I was thinking about something involving an actual center_mass.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:18):

But probably your version is better.

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 04:18):

You can get a center_mass version by rewriting set.finite.convex_hull_eq.

view this post on Zulip Scott Morrison (Jun 04 2020 at 06:54):

I made a bit more progress on Carathéodory, essentially doing the "boring bits", with the actual calculation still to go.

lemma step (t : finset E) (h : findim  E + 1 < t.card) :
  convex_hull (t : set E) =  (x : (t : set E)), convex_hull (t.erase x) :=
-- This is the actual work!
sorry

I'll probably stop for a bit, but if anyone feels like pushing to branch caratheodory2, please go ahead!

view this post on Zulip Jalex Stark (Jun 04 2020 at 07:57):

I poked a bit at your step lemma and found that I wanted a notion of linear_independent for finset, and a theorem saying you can't have independence when the cardinality is too big. (I guess I'm saying this because even though i couldn't find the code, I'm sure someone has thought of this)

I also wanted

lemma finset.card_pos_iff_exists_mem {α : Type u} {s : finset α} :
0 < s.card   a, a  s :=
begin
  have key : 0 < s.card  0 < s.val.card := mem_def,
  rw key, apply multiset.card_pos_iff_exists_mem,
end

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 07:58):

I am just trying to understand the nature of this project. Some dumb questions.

What is the URL for lemma 3.13?

Is "Prove Lemma 3.13, assuming a proof of Lemma 3.12 has been formalised and a statement of Level 3.13 has been formalised" a state which someone with Lean installed properly can render into VS Code on their own PC?

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 07:58):

I am asking if we can go full tactic mode, in some sense

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:00):

I don't think this is the answer to your question, but this is a URL that takes you to lemma 3.13
https://leanprover-community.github.io/sphere-eversion/blueprint/chap-global.html#a0000000047

view this post on Zulip Johan Commelin (Jun 04 2020 at 08:02):

@Jalex Stark relevant thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/linear.20dependence.20of.20more.20than.20dimension/near/199646286

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:03):

Kevin, are you asking for something more sophisticated than "go to the file which has the statement of lemma 3.13 and start filling in a proof"?

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:05):

I think that there should be a prominent link to the Sphere Eversion project at the top of the Leanprover-community website, maybe in some sort of "New (3/6/20): The Sphere Eversion Project" way, with a direct link to Patrick's web page. I want to start promoting the Lean prover community in general. I think that various Lean projects are beginning to pop up and it would be good if google started to notice it and start asking the question "when someone googles Lean do they want to go to the MS dead pages or ours?"

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:09):

@Jalex Stark, I've just pushed a bit more, reducing it closer to some "obvious facts" about linear algebra, and a few easy sorries.

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:10):

As I wanted to state Caratheodory in terms of finsets, we're now running up against some awkwardness that linear algebra is instead about vectors indexed by fintype.

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:11):

There should be a link to the project home page displayed at the top of https://github.com/leanprover-community/sphere-eversion for people who were looking for the project but are terrified of github pages because they are something to do with source code

view this post on Zulip Johan Commelin (Jun 04 2020 at 08:12):

Also... a README

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:12):

The two basic things I'm now missing are:

-- a basic fact about convex hulls of finsets.
lemma quux (t : finset E) (x : E) (m : x  convex_hull (t : set E)) :
   f : E  , ( y, 0  f y)  (t.sum f = 1)  (t.sum (λ e, f e  e) = x) :=
sorry

-- a basic fact about linear algebra!
lemma turkle {t : finset E} (h : findim  E < t.card) :
   f : E  , t.sum (λ e, f e  e) = 0   x  t, f x  0 :=
sorry

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:13):

It would be really great if we can add some easy-to-use hooks that enable people to indicate where work is happening.

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:13):

e.g. that there's a mathlib branch caratheodory2 that people are working on for one of the lemmas

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:14):

sphere-eversion#4
adds a link to the project website from the github

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:15):

We need to make more of an effort to drive people to Patrick's lovely project website.

view this post on Zulip Johan Commelin (Jun 04 2020 at 08:15):

Kevin Buzzard said:

There should be a link to the project home page displayed at the top of https://github.com/leanprover-community/sphere-eversion for people who were looking for the project but are terrified of github pages because they are something to do with source code

Done

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:15):

I'm sorry, I just don't have a clue how to do all of this, but this is how stuff works nowadays.

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:16):

It's next stop Hacker News remember.

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:17):

And maybe Reddit and then maybe some random news source, I've seen this stuff happen now

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:17):

We have to be ready

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:17):

Kevin Buzzard said:

I'm sorry, I just don't have a clue how to do all of this, but this is how stuff works nowadays.

I think it's fine if your comparative advantage is telling people what changes to make.

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:18):

I think quux is not far from set.finite.convex_hull_eq

view this post on Zulip Johan Commelin (Jun 04 2020 at 08:20):

Maybe the landing page of the project should already display the graph...

view this post on Zulip Johan Commelin (Jun 04 2020 at 08:21):

Or a screenshot of the graph that links to the real thing.

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:22):

I genuinely think that the Wikipedia page on sphere eversion should be updated to point to this project. It is the top duck duck go hit for sphere eversion. It doesn't even have to mention Lean. It could just say something about there is an ongoing project to formalise the proof on a computer and then have some link to one of those listy pages of theorems being formalised by computers or whatever they have

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:22):

I don't know the details of how Wikipedia works but I think that that this is newsworthy.

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:23):

Lean gets a mention on this web page https://en.wikipedia.org/wiki/Perfectoid_space and I certainly didn't put that there.

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:25):

Mathematicians need to be pointed to the display of what we can do.

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:28):

Scott Morrison said:

The two basic things I'm now missing are:

-- a basic fact about convex hulls of finsets.
lemma quux (t : finset E) (x : E) (m : x  convex_hull (t : set E)) :
   f : E  , ( y, 0  f y)  (t.sum f = 1)  (t.sum (λ e, f e  e) = x) :=
sorry

-- a basic fact about linear algebra!
lemma turkle {t : finset E} (h : findim  E < t.card) :
   f : E  , t.sum (λ e, f e  e) = 0   x  t, f x  0 :=
sorry

Here's the mathematical content of quux

lemma quux (t : finset E) (x : E) (m : x  convex_hull (t : set E)) :
   f : E  , ( y  t, 0  f y)  (t.sum f = 1)  (t.sum (λ e, f e  e) = x) :=
begin
  rw set.finite.convex_hull_eq (finset.finite_to_set t) at m,
  rcases m with  w, w_nonneg, w_sum_one, w_center ,
end

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:32):

I still don't know how to figure out the correct URL for Lemma 3.13 in the project

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:33):

There are three things left to do to get Carathéodory's theorem

  1. hook up two lemmas to the library API
  2. prove a linear algebra lemma exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card
  3. fill in the sorries, which are all easy facts about inequalities or finsets, in mem_convex_hull_erase

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:33):

  1. is:
lemma exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card {t : finset E} (h : findim  E + 1 < t.card) :
   f : E  , t.sum (λ e, f e  e) = 0  t.sum f = 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

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:35):

As Johan pointed out, your 2 is the topic of this thread
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/linear.20dependence.20of.20more.20than.20dimension/near/199646286

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:36):

(it's not solved there, but people gave pointers to the library that may be useful)

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:36):

@Kevin Buzzard, can you say a little more about your vision for "full tactic mode"?

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:37):

Do you want to click on a lemma in the informal overview and be taken to the lean file that's supposed to contain its formalization?

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:37):

If my browser is in the blueprint web pages and I just want to get back to the main project website, how do I do that? Should there be a link to the main project website from the blueprint?

view this post on Zulip Kevin Buzzard (Jun 04 2020 at 08:38):

I've been too busy with PR, I've not opened the project in VS Code myself yet

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:40):

as far as I can tell, opening the project in VS Code doesn't have any special #mil style formatting or anything like that, I don't know if that's what you were suggesting

view this post on Zulip Scott Morrison (Jun 04 2020 at 08:40):

Thanks @Jalex Stark, I copied and pasted your start to quux in, and did the next few lines.

view this post on Zulip Jalex Stark (Jun 04 2020 at 08:45):

Kevin Buzzard said:

If my browser is in the blueprint web pages and I just want to get back to the main project website, how do I do that? Should there be a link to the main project website from the blueprint?

raised as an issue https://github.com/leanprover-community/sphere-eversion/issues/5

view this post on Zulip Patrick Massot (Jun 04 2020 at 10:45):

I'm sorry I've been ignoring the discussion in this thread since yesterday afternoon. I really wanted to release the website before giving this talk in IAS, but then I had to focus on the talk and then sleep. I know some infrastructure stuff is not as polished as I hoped for. I'll continue working on it of course, and help is welcome (especially since I've been telling my family to be patient for two weeks while I was rushing to get that ready, so I'll have less time for a while). Also on the back-end side there is no continuous integration at all, and building the blue-print website currently requires a non-master branch of plasTeX, but this will all converge pretty quickly I hope (I have full control here since I'm the current maintainer of plasTeX).

view this post on Zulip Patrick Massot (Jun 04 2020 at 10:51):

About the statement of Caratheodory, the project definitely need a version with center_mass. But it can be deduced of another version in terms of convex_hull of course.

view this post on Zulip Patrick Massot (Jun 04 2020 at 10:53):

Kevin Buzzard said:

Is "Prove Lemma 3.13, assuming a proof of Lemma 3.12 has been formalised and a statement of Level 3.13 has been formalised" a state which someone with Lean installed properly can render into VS Code on their own PC?

I don't understand this question.

view this post on Zulip Patrick Massot (Jun 04 2020 at 10:54):

Kevin Buzzard said:

What is the URL for lemma 3.13?

Indeed there is something missing here, I also noticed it yesterday when I had to go to the graph page to figure out the url pointing a lemma I was looking at. I'll fix that.

view this post on Zulip Patrick Massot (Jun 04 2020 at 10:55):

Jalex Stark said:

as far as I can tell, opening the project in VS Code doesn't have any special #mil style formatting or anything like that, I don't know if that's what you were suggesting

It's definitely planned, but I simply didn't have enough time to implement this before the talk, so I released the website anyway.

view this post on Zulip Jalex Stark (Jun 04 2020 at 12:32):

Thanks for the big push, Patrick! I hope your adrenaline levels are settling back into a normal place.

I don't think anyone was expecting these kinds of things to already be ironed out at introduction time. I think Kevin's main point is that people outside of the zulip are going to start paying attention, so maybe we should prioritize features in order of "what will a skeptic complain about us not having" rather than some more natural-seeming prioritization.

Do you think you convinced any of the IAS folks to contribute?

view this post on Zulip Patrick Massot (Jun 04 2020 at 18:03):

I didn't really try to convince people to contribute. The goal was to convince people that we are doing here is interesting.

view this post on Zulip Kevin Kappelmann (Jun 04 2020 at 22:47):

I basically don't understand any of the mathematical content, but I wanted to say: the way you set this up Patrick is just wonderful.

view this post on Zulip Jalex Stark (Jun 04 2020 at 23:34):

I think the button to view the blueprint should be more prominent than the button to go to the github page (if i were confident this was correct, i'd post an issue on github)

view this post on Zulip Scott Morrison (Jun 05 2020 at 00:13):

I'm still not sure how to set this up, but I something that would be lovely would be for each implicit "TODO" item to have a publicly editable text box (ideally not even requiring a PR) for "URL containing active work".

view this post on Zulip Scott Morrison (Jun 05 2020 at 00:14):

This way people could indicate they've started work on some item, by pasting a link to a branch / zulip discussion / twitch stream, whatever, and other people could find and join in.

view this post on Zulip Scott Morrison (Jun 05 2020 at 00:14):

I would love to make it easier and easier for people to work on math in Lean collaboratively.

view this post on Zulip Scott Morrison (Jun 05 2020 at 00:16):

We want the kids to make plans: "Hey let's go do a raid on a corrugation level tonight."

view this post on Zulip Scott Morrison (Jun 05 2020 at 00:18):

("Isn't that a boss level? We might need extra help designing the statement of the big theorem --- let's see if Patrick's free. Oh, and invite Johan, there are going to be some tough big_operator sorries.")

view this post on Zulip Yury G. Kudryashov (Jun 05 2020 at 03:59):

Patrick Massot said:

About the statement of Caratheodory, the project definitely need a version with center_mass. But it can be deduced of another version in terms of convex_hull of course.

We already have set.finite.convex_hull_eq. I suggest adding a finset.convex_hull_eq and make set.finite.convex_hull_eq use it. Then leave Caratheodory with convex_hull, and add a hint in the docs: "you might want to simp only [finset.convex_hull_eq] the RHS ".

view this post on Zulip Yury G. Kudryashov (Jun 05 2020 at 04:09):

#2956

view this post on Zulip Johan Commelin (Jun 05 2020 at 04:55):

Yury G. Kudryashov said:

#2956

It's on the merge queue already

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:16):

Scott Morrison said:

I would love to make it easier and easier for people to work on math in Lean collaboratively.

In case this isn't clear: exploring ways to "make it easier and easier for people to work on math in Lean collaboratively" is very much a goal of this project.

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:20):

About discussing ongoing work, the canonical option is to use GitHub issues, and of course there Zulip which is less structured. The difficulty is to make it easy to add a link to a GitHub issue (or anything else) from the blueprint. It's difficult because the project is currently hosted on GitHub pages which is a static website host, I don't have interactive access to a database here. Any help is welcome.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:21):

Is it possible to make a "Lean blueprint" of this proof?

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:22):

Literally skipping every definition and proof, but getting down the types of definitions and the statements of theorems?

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:23):

I'm not sure this would be so useful. And it would pollute every import statement with sorry warnings.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:24):

@Reid Barton and I were talking about a related thing in Pittsburgh. Sometimes, when you know the right way to set things up, but don't have time to build the theory, you have valuable information: you are capable of being the supervisor of a project, in some sense.

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:24):

I think you can do this locally, but I wouldn't try doing that for the whole project.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:24):

I see. You can play it the following way: you carry in your head what you think are a bunch of good ideas about how things should work, and then people maybe make PRs and if they have missed some tricks then you just tell them at that point

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:25):

In particular I expect the plan to evolve non-trivially while formalizing.

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:26):

No, you can still leave indications. We can even have comments in the Lean files laying out the structure if you have a good idea.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:27):

I really wonder whether we are missing something here. I am interested in proving Lemma 3.13 but not for mathematical reasons.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:29):

If a mathematical expert (with no knowledge about computer proof systems) were to look at the statement of 3.13 and then asked to deduce it from 3.12 they would say it was trivial. And then when we well them that our software cannot even do it they will think that our software is somehow stupid.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:30):

My idea of a computer game is proving theorems in tactic mode. In some sense a milestone for the project will be a situation where the only sorrys are Props.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:31):

At that moment you are true computer game. Definitions are hard for mathematicians.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:32):

Patrick is there some explicit sorried definition which in some sense when filled in would mark the success of the project? Like perfectoid [prime p] X := sorry or whatever we had?

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:33):

The sooner you can advertise a sorry of any form the better.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:34):

Even if it's just some dumb constant Sphere_Eversion, theorem : Sphere_Eversion := sorry or however you want to display it.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:34):

I am still interested in a top-down approach.

view this post on Zulip Mario Carneiro (Jun 05 2020 at 08:34):

I agree with Kevin here. Having a formal plan modulo sorried theorems is already half the battle

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:35):

We are making a plan Mario

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:35):

I thought that having a blueprint was already a good part of the battle.

view this post on Zulip Mario Carneiro (Jun 05 2020 at 08:35):

Of course the statements of the theorems will evolve between this point and the completion

view this post on Zulip Mario Carneiro (Jun 05 2020 at 08:35):

It is

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:36):

Sphere eversion will be spoken of as one of the triumphs if the community pull this off. Patrick do you honestly think sphere eversion is achievable in Lean 3?

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:36):

But sure we can write a lot more Lean code. The Lean code of the project is currently two lines long.

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:36):

Oh yes I hope it is.

view this post on Zulip Mario Carneiro (Jun 05 2020 at 08:36):

Right, it's like groundbreaking in a construction project

view this post on Zulip Mario Carneiro (Jun 05 2020 at 08:36):

you have the blueprint, now you need the physical scaffolding

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:37):

Patrick's approach is what mathematicians need. Many of us think very vaguely but Patrick has learnt a really good way of expressing mathematics in a format humans understand and yet is good enough for others to be able to join in

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:37):

I came along and asked for localications of rings because I had a blueprint for schemes. Two years later look at what @Amelia Livingston has done.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:38):

My blueprint was just in my head, so it was realised by people close to me like @Chris Hughes and @Kenny Lau . They were all at Imperial and I was too busy to write it all down properly.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:39):

So I just taught them. Patrick is enabling this teaching to take place online.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:39):

My blueprint for schemes turned into a much better understanding of the concept of a localisation of a ring

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:40):

Patrick's project just opens more doors I think.

view this post on Zulip Patrick Massot (Jun 05 2020 at 08:42):

Right now I need to do a lot of stuff that I neglected while I was rushing to get this stuff out. But then I'll go through the blueprint to polish it. I also hope that Sébastien, Reid, Yury and Heather will have a look (we have seen Heather for a while, I should make sure she saw this thread).

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:54):

"The easiest example of a flexible construction problem which is not totally trivial and is algebraically obstructed is the deformation of immersions of circles into planes. " Is it possible to give some Wikipedia link to the definition of an immersion? This term has a precise meaning, right?

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 08:55):

Or maybe some kind of hover thing giving a precise definition?

view this post on Zulip Kyle Miller (Jun 05 2020 at 10:17):

Kevin Buzzard said:

"The easiest example of a flexible construction problem which is not totally trivial and is algebraically obstructed is the deformation of immersions of circles into planes. " Is it possible to give some Wikipedia link to the definition of an immersion? This term has a precise meaning, right?

It looks like the three sentences following that one are meant to be the definition. (In general, an immersion f:XYf:X \to Y is a smooth function whose differential df:TXTYdf:TX\to TY is everywhere injective. "Deformations" refers to smooth homotopies through the space of immersions, i.e. smooth maps F:[0,1]×XYF: [0,1]\times X\to Y such that ft(x)=F(t,x)f_t(x)=F(t,x) is an immersion for each tt. Such homotopies are known as regular homotopies.)

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:26):

@Patrick Massot I would really like a sorry to be able to point people to, for a blog post. "That's the goal"

view this post on Zulip Patrick Massot (Jun 05 2020 at 10:47):

Yes the three sentences following that one are meant to explain the words.

view this post on Zulip Patrick Massot (Jun 05 2020 at 10:47):

And the general explanation is in https://leanprover-community.github.io/sphere-eversion/blueprint/sect0001.html#a0000000003 and the next line.

view this post on Zulip Patrick Massot (Jun 05 2020 at 10:49):

We can't yet state the sphere eversion theorem because mathlib doesn't know that S2\mathbb S^2 is a manifold, and doesn't know about immersions. But we can certainly sprint towards that.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:52):

Right -- just sorry the definitions, hide them away, assume that people know the specification but not the implementation.

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:53):

And find a juicy-looking theorem and say the proof is sorry and it can somehow be the flagship thing

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 10:54):

and you could run a comedy clone of the webserver which when you fire it up just has the theorem statement and sorried proof and challenge all-comers to fill in the sorry

view this post on Zulip Scott Morrison (Jun 05 2020 at 11:08):

mathematical deathmatch!

view this post on Zulip Kevin Buzzard (Jun 05 2020 at 11:16):

if some crank says that they can prove sphere eversion using Fermat's Last Theorem then you can tell them to go ahead and fill in the sorry

view this post on Zulip Jalex Stark (Jun 05 2020 at 14:55):

one reason we don't have much lean code in the repo is because e.g. caratheodory development is happening in mathlib

view this post on Zulip Jalex Stark (Jun 05 2020 at 14:55):

it would be nice later (or, right now, really) to have evidence that this mathlib development was caused by the sphere eversion project

view this post on Zulip Jalex Stark (Jun 05 2020 at 14:56):

(I don't have an idea how to implement that, just throwing out an open problem in "mathematical MMO design theory")

view this post on Zulip Patrick Massot (Jun 05 2020 at 15:30):

In the perfectoid project we tried to say explicitly in PR messages when it came from the project. But sometimes we forgot.

view this post on Zulip Bhavik Mehta (Jun 05 2020 at 15:37):

In my PRs from projects I've usually included that it's come from a project, but I'm not sure how helpful that is for Jalex's goal?

view this post on Zulip Jalex Stark (Jun 05 2020 at 15:40):

to clarify, my goal is that an outsider should be able to tell, right now, that caratheodory has significant progress. I suppose it would be enough to have an earlier suggestion of kevin, which was something like:
on each lemma tracked in the blueprint, let people leave comments saying things like "I am working on this in the caratheodory2 branch of mathlib"

view this post on Zulip Jalex Stark (Jun 05 2020 at 15:41):

like the comments on this book (the book is about hg, a git alternative. The commenting is implemented in hg instead of in git, so can't be copied to use out-of-the-box)

view this post on Zulip Yury G. Kudryashov (Jun 05 2020 at 16:58):

Can we generate a GitHub issue per node and add links to these issues?

view this post on Zulip Patrick Massot (Jun 05 2020 at 17:01):

I don't think we should create issues a priori since it would make an unmanageable list, but we can certainly create them as soon as someone starts discussing something in particular.

view this post on Zulip Johan Commelin (Jun 06 2020 at 07:25):

@Patrick Massot In the graph https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph.html why does theilliere have a blue background, if it depends on the definition corrugation that hasn't been done yet...?

view this post on Zulip Patrick Massot (Jun 06 2020 at 08:30):

It means that the proof will be ready to be formalized as soon as the statement will be there. I know it looks a bit silly, but I wanted to convey the idea that formalizing the statement should be somehow prioritized since we will then be able to play proving it right away.

view this post on Zulip Johan Commelin (Jun 06 2020 at 08:32):

Aha. Thanks.

view this post on Zulip Patrick Massot (Jun 06 2020 at 08:34):

I'm open to other color coding suggestions of course, especially in this special case where it's clearly confusing.

view this post on Zulip Johan Commelin (Jun 06 2020 at 08:41):

Patrick Massot said:

I'm open to other color coding suggestions of course, especially in this special case where it's clearly confusing.

My gut reaction is to just leave the interior white. Take something like one_jet_extension_prop... that still has a decent amount of dependencies that need to be done first.

view this post on Zulip Scott Morrison (Jun 06 2020 at 08:46):

@Patrick Massot, I think Lemma 1.4 is not the statement you want.

As it's written, it's trivially true, because it says "at most (d+1) points" --- you just use Lemma 1.3, and discard the points with coefficient zero.
It's not true if you change the statement to say "exactly (d+1) points" (take the intersection of the diagonals in a convex quadrilateral in R^2).

Because in later applications we really need it to say "exactly (d+1) points" (because the essential fact is that the point is in the interior of a simplex), presumably Lemma 1.4 is meant to have stronger hypotheses, e.g. that P itself is open, as well as a stronger conclusion "exactly (d+1) points". Then the theorem becomes both true and useful. :-)

view this post on Zulip Patrick Massot (Jun 06 2020 at 08:48):

Indeed. And you can see from the "proof" that I wrote that statement in a hurry and wasn't happy about it.

view this post on Zulip Scott Morrison (Jun 07 2020 at 04:30):

I just made a PR to the sphere-eversion project which takes Patrick's human proof of lem:int_cvx and turns it into a Lean file with lots of sorries.

view this post on Zulip Scott Morrison (Jun 07 2020 at 04:31):

None of the statements have sorry, and I think it would be reasonable for someone to finish off this file without having to introduce any new declarations. (i.e. nothing should take more than 10 lines to prove :-)

view this post on Zulip Scott Morrison (Jun 07 2020 at 04:32):

As @Kevin Buzzard was discussing above, I hope files like this are useful intermediate steps between the human readable blueprint and a compilable Lean file.

view this post on Zulip Patrick Massot (Jun 07 2020 at 17:40):

Thanks Scott!

view this post on Zulip Patrick Massot (Jun 07 2020 at 17:41):

I think this is indeed a very good way to move the project forward. It even allows even more contributors to work on the project, since proving stuff is rather easier than writing definitions and statements in the right way.

view this post on Zulip Patrick Massot (Jun 07 2020 at 17:42):

I also love the idea that we could this as an excuse to improve and battle test our young affine geometry library. @Joseph Myers did you see that PR?

view this post on Zulip Joseph Myers (Jun 07 2020 at 18:06):

I certainly expect there is some overlap between affine combinations of points as needed for barycentric coordinates for geometry (PR #2979), and whatever's needed for convexity (issue #2910).

Defining homotheties in affine spaces (dilation in that PR) is on my list of things that obviously should be added to fill out the affine space implementation, but isn't done yet (although it's trivial).

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 18:28):

@Patrick Massot how do you feel about putting in italics the words being defined in a definition? I rather like this style but you use it sparingly. I'm currently on an exercise bike looking at the blueprint on a tablet and it looks really good

view this post on Zulip Patrick Massot (Jun 07 2020 at 19:02):

Sure, I also like this. But I guess I wasn't systematic here.

view this post on Zulip Yury G. Kudryashov (Jun 07 2020 at 19:18):

I have a branch with dilation, const, line_map affine maps and monoid structure on affine self-maps. I'll push it tonight.

view this post on Zulip Yury G. Kudryashov (Jun 07 2020 at 23:33):

#2981

view this post on Zulip Yury G. Kudryashov (Jun 08 2020 at 00:09):

I started porting convexity to affine spaces, see branch convex-affine. It should be ported to line_map from #2981 and affine combinations of points from #2979.

view this post on Zulip Patrick Massot (Jun 08 2020 at 08:54):

@Scott Morrison What do you prefer with https://github.com/leanprover-community/sphere-eversion/pull/8, should I wait for all these mathlib PR to be merged first or would you prefer that I merge the this PR and modify stuff later?

view this post on Zulip Scott Morrison (Jun 08 2020 at 08:55):

My suggestion would be to merge earlier rather than later. I don't particularly mind, but for other contributors I'd suggest setting a "lower bar" for PRs etc to be accepted to a "blueprint project" than to something like mathlib.

view this post on Zulip Scott Morrison (Jun 08 2020 at 08:56):

I haven't even had a change to look at the affine combinations PR, so haven't thought about how to adapt to that.

view this post on Zulip Patrick Massot (Jun 08 2020 at 08:57):

Ok I don't mind merging. Any preference about squashing?

view this post on Zulip Johan Commelin (Jun 08 2020 at 08:58):

I think I have a slight preference for not squashing.

view this post on Zulip Scott Morrison (Jun 08 2020 at 09:24):

I guess I was going to say slight preference for squashing, but it's very weak.

view this post on Zulip Joseph Myers (Jun 08 2020 at 11:50):

As that sphere-eversion PR includes a sorry definition of affine_independent, I'll note I did start writing a definition of affine_independent for geometry purposes but it hasn't got far enough yet to be useful (and I don't guarantee what's there is correct). In case it's useful:

import linear_algebra.affine_space
open add_torsor

variables (k : Type*) (V : Type*) {P : Type*} [ring k] [add_comm_group V] [module k V]
variables [S : affine_space k V P]
include S

/-- Whether the points in an indexed family, minus a given base point,
produce linearly independent vectors. -/
def vsub_linear_independent {ι : Type*} (p : P) (f : ι  P) : Prop :=
linear_independent k (λ i, (f i - p : V))

/-- If the base point is in the indexed family,
`vsub_linear_independent` for the rest of that family does not depend
on the choice of base point. -/
lemma vsub_linear_independent_of_vsub_linear_independent {ι : Type*} (i1 i2 : ι) (f : ι  P)
    (h : vsub_linear_independent k V (f i1) (λ i : {x // x  i1}, f i)) :
  vsub_linear_independent k V (f i2) (λ i : {x // x  i2}, f i) :=
begin
  unfold vsub_linear_independent at *,
  rw linear_independent_iff',
  rw linear_independent_iff' at h,
  intros s g hs i hi,
  conv_lhs at hs {
    congr,
    skip,
    funext,
    rw [vsub_sub_vsub_right_cancel V _ _ (f i1), smul_sub]
  },
  sorry
end

/-- Whether the points in an indexed family are affinely
independent. This definition means an empty family is affinely
independent. -/
def affine_independent {ι : Type*} (f : ι  P) : Prop :=
 (i : ι), vsub_linear_independent k V (f i) (λ j : {x // x  i}, f j)

view this post on Zulip Scott Morrison (Jun 09 2020 at 03:05):

Is this going to go in a PR soon? How about we update the sorry in the sphere-eversion file once it's in a PR and/or mathlib.

view this post on Zulip Patrick Massot (Jun 09 2020 at 09:52):

I think I'm done with url generation, see eg this change which then generates this url. It means the LaTeX command \lean now takes a list of fully qualified Lean names and will build urls. Those names have to be in scope when you import all files from the sphere eversion project, hence it won't work with mathlib declaration from files not (transitively) imported by the project.

I apologize to @Rob Lewis because in the end I don't use his export.json. I didn't think carefully enough before asking. I doesn't make sense to use his file since I need to pinpoint a mathlib commit, otherwise mathlib will move faster than the TeX file and data will get out of sync.

view this post on Zulip Patrick Massot (Jun 09 2020 at 09:55):

I also apologize for not writing (non-meta) Lean code for this project. All my Lean time is still taken up by infrastructure work, but this should improve soon (next week or earlier) since I hope we are now happy with the infrastructure (but it still needs some more cleanup in the leanblueprint plasTeX plugin) and I only have one last exam to mark and I'll be done with hiring committees on Thursday night.

view this post on Zulip Joseph Myers (Jun 09 2020 at 12:46):

There are a few other things I'll probably do with affine spaces and geometry before getting back to affine independent families, so feel free to pick up affine independence if you'd like it working sooner.

view this post on Zulip Johan Commelin (Jun 10 2020 at 18:22):

@Heather Macbeth By the way... have you seen this thread?

view this post on Zulip Heather Macbeth (Jun 10 2020 at 18:24):

Yes, I have, I am interested to join. I hope that at some point I can contribute to Lean's manifold libraries, and perhaps in particular do some of the manifold things needed for the sphere eversion project.

view this post on Zulip Joseph Myers (Jun 21 2020 at 16:01):

I do now have a working definition of affine_independent, and a proof relating affine_independent and linear_independent (longer than I'd like, and depends on #3122 for the definition and #3124 for the proof), ready to PR once those two PRs are in.

/-- An indexed family is said to be affinely independent if no
nontrivial weighted subtractions (where the sum of weights is 0) are
0. -/
def affine_independent {ι : Type*} (p : ι  P) : Prop :=
 (s : finset ι) (w : ι  k) (h :  i in s, w i = 0), s.weighted_vsub V w p = 0   i  s, w i = 0

/-- A family is affinely independent if and only if the differences
from a base point in that family are linearly independent. -/
lemma affine_independent_iff_linear_independent_vsub {ι : Type*} (p : ι  P) (i1 : ι) :
  affine_independent k V p  linear_independent k (λ i : {x // x  i1}, (p i - p i1 : V)) :=
by sorry -- long proof omitted here

view this post on Zulip Patrick Massot (Jun 26 2020 at 15:39):

I've been greenwashing the dependency graph. As usual with greenwashing, this is pretty superficial. I wrote definitions and stated theorems, but haven't proved anything. As usual, you can see the next targets. The preliminaries part is still waiting for some affine geometry PRs but it should move forward soon.

view this post on Zulip Bhavik Mehta (Jun 26 2020 at 15:41):

Is there a maths proof somewhere for Lemma 2.13?

view this post on Zulip Patrick Massot (Jun 26 2020 at 15:41):

We will also need to glue https://github.com/leanprover-community/sphere-eversion/blob/master/src/loops/int_cvx.lean to https://github.com/leanprover-community/sphere-eversion/blob/master/src/loops/basic.lean#L32-L43

view this post on Zulip Patrick Massot (Jun 26 2020 at 15:42):

Bhavik Mehta said:

Is there a maths proof somewhere for Lemma 2.13?

Good point, I forgot to write it. Of course the real world proof is: this is obviously obvious. But at some point I also thought about a nice Lean path. I need to remember it and write it down.

view this post on Zulip Jalex Stark (Jun 26 2020 at 15:43):

if i'm looking at the blueprint and see a statement with a green border, what's the intended way for me to pull up the lean statement?

view this post on Zulip Patrick Massot (Jun 26 2020 at 15:49):

Hmm, it needs quite a lot of clicks. Clicking the node will show the math statement. Clicking the header brings the blueprint page, clicking Lean next to the header shows the link to GitHub.

view this post on Zulip Patrick Massot (Jun 26 2020 at 15:49):

I could easily save a couple of clicks here.

view this post on Zulip Jalex Stark (Jun 26 2020 at 15:58):

it would be amazing if clicking the node would show the math statement and the lean statement

view this post on Zulip Patrick Massot (Jun 26 2020 at 16:00):

Showing a link to GitHub is easy (and already done from the main text). Going further would require more work. It's nothing impossible of course, as proven by mathlib docs, but I already spent a lot of time on this infrastructure, and now I need to prove stuff.

view this post on Zulip Patrick Massot (Jun 26 2020 at 16:32):

@Bhavik Mehta I pushed a LaTeX proof. I think this is a very nice target. It will be helpful to the topology library (I think we don't have path-connected components) and linear algebra. Of course there should be many preliminaries Lean lemmas.

view this post on Zulip Patrick Massot (Jun 26 2020 at 18:13):

Great, Bhavik opened a WIP PR.

view this post on Zulip Bhavik Mehta (Jun 26 2020 at 18:15):

I should say this is pretty much one of the first times I'm using this bit of mathlib, so it's entirely possible that some of my proofs can be shortened/improved!

view this post on Zulip Patrick Massot (Jun 26 2020 at 18:26):

Defining path components of sets is tricky because there are so many options. In addition to what Bhavik did in his PR, consider the following two options:

import topology.instances.real

open_locale classical topological_space filter
open filter set
variables {X : Type*} [topological_space X]

local notation `I` := Icc (0 : ) 1

/-!
## Using a structured predicate on ℝ → X
-/

/-- A path `γ` joins `x` to `y` in `F` -/
structure joins_in (γ :   X) (x y : X) (F : set X) : Prop :=
(cont : continuous_on γ I)
(src : γ 0 = x)
(tgt : γ 1 = y)
(inside :  t  I, γ t  F)

def joined_in (F : set X) : X  X  Prop :=
λ x y,  γ :   X, joins_in γ x y F

/-!
## Using bundled paths
-/

/-- A continuous path in `F` -/
structure path (F : set X) :=
(to_fun :   X)
(cont' : continuous_on to_fun I)
(inside' :  t  I, to_fun t  F)

instance (F : set X) : has_coe_to_fun  (path F) :=
⟨_, path.to_fun

-- Now restate fields of path in terms of the coercion

lemma path.cont {F : set X} (γ : path F) : continuous_on γ I := γ.cont'

lemma path.inside {F : set X} (γ : path F) :  t  I, γ t  F := γ.inside'

def joined_in' (F : set X) : X  X  Prop :=
λ x y,  γ : path F, γ 0 = x  γ 1 = y

This is only scratching the surface of design space like Leo would say.

view this post on Zulip Patrick Massot (Jun 26 2020 at 18:27):

Everybody is welcome to come up with alternative designs and, more importantly, try to manipulate it. The first milestone is to prove this gives an equivalence relation. Next prove a couple of simple sets are connected.

view this post on Zulip Patrick Massot (Jun 26 2020 at 18:28):

Note the common point of those alternative approaches is to avoid subtypes everywhere (source and target).

view this post on Zulip Patrick Massot (Jun 26 2020 at 18:29):

I think it's a pretty safe bet, but I may be wrong.

view this post on Zulip Bhavik Mehta (Jun 26 2020 at 18:30):

I think what makes me nervous about these is that it might be awkward to define γ on all of R, although if we provide a constructor allowing one to define it on [0,1] instead this could be alright

view this post on Zulip Bhavik Mehta (Jun 26 2020 at 18:30):

I agree that the subtypes in my version aren't the most pleasant though

view this post on Zulip Bhavik Mehta (Jun 26 2020 at 18:34):

For what it's worth, my vote goes to the bundled path approach above

view this post on Zulip Patrick Massot (Jun 26 2020 at 19:05):

I'm serious when I write we shouldn't vote before trying all three approaches (and maybe one more).

view this post on Zulip Patrick Massot (Jun 26 2020 at 19:06):

About defining only on [0, 1], I claim that if you can prove transitivity of the relation then it won't matter. The only explicit constructions will be affine maps.

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 19:59):

An approach was already explored in #1160.

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 20:00):

See in particular the comments by Reid there.

view this post on Zulip Patrick Massot (Jun 26 2020 at 22:25):

I'll read that, but we don't need anything that looks even remotely like homotopy theory here.

view this post on Zulip Patrick Massot (Jun 29 2020 at 11:19):

@Bhavik Mehta do you intend to work on that soon? Or would you prefer that I setup path connected component and then you try to prove stuff from the project?

view this post on Zulip Bhavik Mehta (Jun 29 2020 at 15:55):

I made a bit more progress but I wasn't sure that there's much point in me continuing to prove things about path connectivity if we're going to change the definition later on

view this post on Zulip Bhavik Mehta (Jun 29 2020 at 15:57):

I think though that I'm probably not the best person to explore how good different definitions are for topology since I don't know the topology library at all well

view this post on Zulip Patrick Massot (Jun 29 2020 at 15:57):

Did you try to prove transitivity?

view this post on Zulip Patrick Massot (Jun 29 2020 at 15:58):

Did you want to play with the linear algebra part of this lemma instead?

view this post on Zulip Bhavik Mehta (Jun 29 2020 at 16:01):

I did and the annoying part for me was showing continuity - I think it was because the gluing lemma and continuity of subtypes was tricky to me; but this might be me not understanding/finding the right lemmas

view this post on Zulip Bhavik Mehta (Jun 29 2020 at 16:01):

For instance I also struggled with https://github.com/leanprover-community/sphere-eversion/pull/10/files#diff-c7f593664d2edfb1c442be00f422be93R42

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:02):

Of course continuity is the annoying part, there is nothing else!

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 16:07):

Again, all this is already done in #1160.

view this post on Zulip Patrick Massot (Jul 01 2020 at 16:18):

@Bhavik Mehta I just pushed an experiment in https://github.com/leanprover-community/sphere-eversion/commit/9d4fde464db108e4aae1ab5cf5a9449a429031ba. There is one file that proves a rather general gluing lemma for continuous_on. The proof needs cleaning up (there is a big almost duplicate chunk in the middle) but we'll need the statement a lot in other places of the project. Then there is a file about path connected sets which is an easy application (the gluing lemma is used to concatenate paths). The main theme of this approach is to avoid subtypes everywhere. Every data is global and conditions are enforced only on subsets. I'm not yet fully convinced this is the way to go, but at least there is no coercion to fight (since coercions to functions now work). I hope this can get you unstuck on the way to the part you feel comfortable working on.

view this post on Zulip Bhavik Mehta (Jul 01 2020 at 16:21):

Wonderful, looks great, thanks!

view this post on Zulip Reid Barton (Jul 01 2020 at 16:23):

What's the purpose of F rather than just using the whole space?

view this post on Zulip Reid Barton (Jul 01 2020 at 16:24):

As far as I can see, removing F makes everything simpler

view this post on Zulip Bhavik Mehta (Jul 01 2020 at 16:24):

I think it makes it easier to speak about path connected subsets

view this post on Zulip Reid Barton (Jul 01 2020 at 16:24):

It doesn't look easier though.

view this post on Zulip Bhavik Mehta (Jul 01 2020 at 16:25):

The alternative is to use the subspace topology which is against the main theme

view this post on Zulip Bhavik Mehta (Jul 01 2020 at 16:25):

As far as I can tell

view this post on Zulip Reid Barton (Jul 01 2020 at 16:25):

Yes, use the subspace topology.

view this post on Zulip Reid Barton (Jul 01 2020 at 16:26):

For functions out of a subspace I can kind of understand these oblique methods, but for functions into a subspace they don't seem to gain anything.

view this post on Zulip Reid Barton (Jul 01 2020 at 16:26):

By the way, it's harmless to define the path as a continuous function on the whole real line since you can map the reals to [0, 1] continuously and preserving 0 and 1.

view this post on Zulip Patrick Massot (Jul 01 2020 at 16:38):

Yes, I wanted to also try with using the subspace topology. This is not the really complicated part anyway. The gluing lemma is more complicated than I would like. But your continuity trick could help here, I definitely didn't think about it.

view this post on Zulip Patrick Massot (Jul 01 2020 at 16:38):

All these discussions are so unnatural from a mathematical perspective where moving between types and subtypes is completely transparent.

view this post on Zulip Johan Commelin (Jul 04 2020 at 06:31):

Another nice animation: https://rreusser.github.io/explorations/sphere-eversion/

view this post on Zulip Jean Lo (Jul 14 2020 at 15:07):

hi! after some tragic struggles, I've very recently regained the ability to actually run Lean. I was hoping there might be something I can do that can possibly be helpful for this project. is there any other ongoing work I should be aware of, in addition to the discussion here & what's in the repository so far?

I spent some time last year prodding at #1160 as well as other previous approaches towards paths-y stuff (https://github.com/ImperialCollegeLondon/xena-UROP-2018/tree/master/src/Topology), so I looked at the blueprint and started out trying have a go at some of the sorries in loops/surrounding, and then I realised I didn't have some Elementary Topology Facts™. I sidetracked and started writing some of those down:

https://github.com/leanprover-community/sphere-eversion/pull/11

I feel that not having to worry about functions out of a unit-interval subtype with this formulation was nice, but some of the stuff I wrote down myself involving relative-open-ness and nhds_within felt maybe a little dubious? There are comments; hopefully those would be helpful even if the code isn't very, as just an example of someone naively trying to work with the implementation.

view this post on Zulip Patrick Massot (Jul 14 2020 at 18:08):

HI! This project has not moved recently because all my Lean time has been devoted to preparing the workshop. But I'll certainly return to it and you are very welcome.

view this post on Zulip Patrick Massot (Jul 14 2020 at 18:09):

Next week I'm meant to be in vacations but I'll try to move this project forward a bit.

view this post on Zulip Johan Commelin (Aug 27 2020 at 18:12):

I was looking at the graph again https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph.html and I'm excited to see that there's already quite a lot of blue there! (And also a bunch of green borders, which means that those are sorrys whose statement is done, but the proof has to be filled in.)

view this post on Zulip Patrick Massot (Aug 27 2020 at 18:54):

Yes, I defined a bunch of things and stated quite a few lemmas, hoping it would be easier to contribute proofs, but up to now nobody proved much. I've been working of the mathlib side however, as you can see here. I need to finish the determinant series, but I'm working on integration in parallel. I have a proof of the main theorem about differentiation under the integral sign modulo the theorem claiming you can commute integration and applying a continuous linear map. Unfortunately the later result is very close to the construction and I'm waiting for help from either Sébastien or Yury.

view this post on Zulip Patrick Massot (Aug 27 2020 at 19:03):

Oh, I just saw Anatole opened a PR three hours ago!

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 20:16):

I'll look into the "commute" statement. I also need it but for a different reason: I want to prove that the integral of a "uniformly analytic" family of functions is analytic.

view this post on Zulip Patrick Massot (Sep 15 2020 at 20:17):

Oh I have a proof of the commute statement.

view this post on Zulip Patrick Massot (Sep 15 2020 at 20:17):

My last 5 PRs or so are working towards this.

view this post on Zulip Patrick Massot (Sep 15 2020 at 20:18):

It was a nightmare until Floris proved his induction principle for integrable functions.

view this post on Zulip Patrick Massot (Sep 15 2020 at 20:19):

Do you want to see the proof?

view this post on Zulip Patrick Massot (Sep 15 2020 at 20:23):

Actually I think I have enough preliminaries for the commutation lemma now. So I need one PR for this lemma, one calculus preliminaries PR and then one PR differentiating under integrals.

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 20:43):

What induction principle are you talking about?

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 20:45):

Found #3978

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 20:50):

Could you please paste the statement of the commute lemma here? What typeclasses do you assume?

view this post on Zulip Patrick Massot (Sep 15 2020 at 20:59):

continuous_linear_map.integral_apply_comm :
   {α : Type*} [measurable_space α] {μ : measure α} {E : Type*} [normed_group E]
  [second_countable_topology E] [normed_space  E] [complete_space E]
  [measurable_space E] [borel_space E] {F : Type*} [normed_group F]
  [second_countable_topology F] [normed_space  F] [complete_space F]
  [measurable_space F] [borel_space F] {φ : α  E} (L : E L[] F),
    measurable φ  integrable φ μ   (a : α), L (φ a) μ = L ( (a : α), φ a μ)

view this post on Zulip Patrick Massot (Sep 15 2020 at 21:00):

And of course there is a version with (φ : α →₁[μ] E)

view this post on Zulip Patrick Massot (Sep 15 2020 at 21:02):

import measure_theory.set_integral

noncomputable theory

open topological_space measure_theory filter metric
open_locale topological_space filter nnreal big_operators

variables {α : Type*} [measurable_space α] {μ : measure α}
variables {E : Type*} [normed_group E] [second_countable_topology E] [normed_space  E]
          [complete_space E] [measurable_space E] [borel_space E]
variables {F : Type*} [normed_group F] [second_countable_topology F] [normed_space  F]
  [complete_space F] [measurable_space F] [borel_space F]


namespace measure_theory

lemma integrable.clm_apply {φ : α  E} (φ_int : integrable φ μ)
  (L : E L[] F) : integrable (λ (a : α), L (φ a)) μ :=
((integrable.norm φ_int).const_mul L).mono' (eventually_of_forall $ λ a, L.le_op_norm (φ a))

def l1.clm_apply (φ : α [μ] E) (L : E L[] F) : α [μ] F :=
l1.of_fun (λ a, L (φ a)) (φ.measurable.clm_apply L) (φ.integrable.clm_apply L)

lemma l1.clm_apply_apply (φ : α [μ] E) (L : E L[] F) :  a μ, (φ.clm_apply L) a = L (φ a) :=
l1.to_fun_of_fun _ _ _

-- The next lemma is a bit silly since the conclusion holds everywhere, but this weakening is
-- useful
lemma l1.norm_clm_apply_le (φ : α [μ] E) (L : E L[] F) :  a μ, L (φ a)  L*φ a :=
eventually_of_forall (λ a, L.le_op_norm (φ a))

lemma l1.measurable_clm_apply (L : E L[] F) (φ : α [μ] E): measurable (φ.clm_apply L) :=
(φ.clm_apply L).measurable

lemma l1.measurable_clm_apply' (L : E L[] F) (φ : α [μ] E): measurable (λ a, L (φ a)) :=
L.measurable.comp φ.measurable

lemma l1.integrable_clm_apply (L : E L[] F) (φ : α [μ] E): integrable (φ.clm_apply L) μ :=
(φ.clm_apply L).integrable

lemma l1.integrable_clm_apply' (L : E L[] F) (φ : α [μ] E): integrable (λ a, L (φ a)) μ :=
φ.integrable.clm_apply L

lemma l1.integral_clm_apply (φ : α [μ] E) (L : E L[] F):
   a, (φ.clm_apply L) a μ =  a, L (φ a) μ :=
by simp [l1.clm_apply]

def l1.clm_applyₗ (L : E L[] F) : (α [μ] E) [] (α [μ] F) :=
{ to_fun := λ φ, φ.clm_apply L,
  map_add' := begin
    intros f g,
    dsimp [l1.clm_apply],
    rw [ l1.of_fun_add, l1.of_fun_eq_of_fun],
    apply (l1.add_to_fun f g).mono,
    intros a ha,
    simp only [ha, pi.add_apply, L.map_add]
  end,
  map_smul' := begin
    intros c f,
    dsimp [l1.clm_apply],
    rw [ l1.of_fun_smul, l1.of_fun_eq_of_fun],
    apply (l1.smul_to_fun c f).mono,
    intros a ha,
    simp only [ha, pi.smul_apply, continuous_linear_map.map_smul]
  end }

lemma l1.clm_apply_norm_le (φ : α [μ] E) (L : E L[] F) : φ.clm_apply L  L*φ :=
begin
  erw l1.norm_of_fun_eq_integral_norm,
  calc
   a, L (φ a) μ   a, L *φ a μ : integral_mono (L.measurable.comp φ.measurable).norm
                                (φ.integrable_clm_apply' L).norm (φ.measurable_norm.const_mul $ L)
                                (φ.integrable_norm.const_mul $ L) (φ.norm_clm_apply_le L)
  ... = L * φ : by rw [integral_mul_left, φ.norm_eq_integral_norm]
end

end measure_theory

open measure_theory

variables (μ)

def continuous_linear_map.l1_apply (L : E L[] F) : (α [μ] E) L[] (α [μ] F) :=
linear_map.mk_continuous (measure_theory.l1.clm_applyₗ L) (L) (λ φ, φ.clm_apply_norm_le L)

lemma continuous_linear_map.continuous_integral_apply (L : E L[] F) :
continuous (λ (φ : α [μ] E),  (a : α), L (φ a) μ) :=
begin
  rw  funext (λ φ : α [μ] E, φ.integral_clm_apply L),
  exact continuous_integral.comp (L.l1_apply μ).continuous
end

variables {μ}

lemma continuous_linear_map.integral_apply_comm {φ : α  E} (L : E L[] F) (φ_meas : measurable φ)
  (φ_int : integrable φ μ) :  a, L (φ a) μ = L ( a, φ a μ) :=
begin
  refine integrable.induction _ _ _ _ φ_meas φ_int,
  { intros e s s_meas s_finite,
    rw [integral_indicator_const e s_meas, continuous_linear_map.map_smul,
         integral_indicator_const (L e) s_meas],
    congr' 1,
    ext a,
    rw set.indicator_comp_of_zero L.map_zero },
  { intros f g H f_meas g_meas f_int g_int hf hg,
    simp [L.map_add, integral_add f_meas f_int g_meas g_int,
      integral_add (f_meas.clm_apply L) (f_int.clm_apply L)
      (g_meas.clm_apply L) (g_int.clm_apply L), hf, hg] },
  { exact is_closed_eq (L.continuous_integral_apply μ)  (L.continuous.comp continuous_integral) },
  { intros f g hfg f_meas g_meas f_int hf,
    convert hf using 1 ; clear hf,
    { exact integral_congr_ae (L.measurable.comp g_meas) (L.measurable.comp f_meas) (hfg.fun_comp L).symm },
    { rw integral_congr_ae g_meas f_meas hfg.symm } }
end

lemma continuous_linear_map.l1_integral_apply_comm (L : E L[] F) (φ : α [μ] E) :
   a, L (φ a) μ = L ( a, φ a μ) :=
L.integral_apply_comm φ.measurable φ.integrable

view this post on Zulip Patrick Massot (Sep 15 2020 at 21:02):

I don't have time to make a PR today but you can already comment on the above code if you want. This should work with a modern mathlib.

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 21:05):

Thank you!

view this post on Zulip Patrick Massot (Sep 15 2020 at 21:14):

Is that version suitable for your use?

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 21:32):

Most probably yes but there may be difficulties.

view this post on Zulip Yury G. Kudryashov (Sep 15 2020 at 21:34):

(e.g., I'm not sure yet what [second_countable_topology] assumption I'll need).

view this post on Zulip Patrick Massot (Sep 15 2020 at 22:21):

Both second countability assumptions are needed to even write the integrals from the statement, unless you redo Bochner integration without second countability. Did you notice #4099?

view this post on Zulip Patrick Massot (Sep 16 2020 at 09:18):

I opened #4167

view this post on Zulip Yury G. Kudryashov (Sep 22 2020 at 03:39):

One more way to prove lemmas about integrals is in #4199: the new proof in simple_func_dense actually states that the sequence of functions approximating f : α → E does not depend on μ : measure α. This makes the proofs dealing with different measures much shorter.

view this post on Zulip Patrick Massot (Sep 22 2020 at 07:15):

Very nice!

view this post on Zulip Patrick Massot (Sep 22 2020 at 07:17):

But we should really decide something about #4170 (add measurable to integrable). @Sebastien Gouezel I think we are waiting for your opinion there.

view this post on Zulip Sebastien Gouezel (Sep 22 2020 at 07:33):

I think it is a very good idea, but I haven't looked at the details. I'm willing to trust Floris on this, though, and fix things later if needed.

view this post on Zulip Johan Commelin (Sep 25 2020 at 09:41):

Yury G. Kudryashov said:

I started porting convexity to affine spaces, see branch convex-affine. It should be ported to line_map from #2981 and affine combinations of points from #2979.

Do you still have a copy of that convex-affine branch locally?

view this post on Zulip Yury G. Kudryashov (Sep 25 2020 at 18:30):

Yes, I'll reopen the pr tomorrow

view this post on Zulip Johan Commelin (Oct 06 2020 at 12:25):

@Yury G. Kudryashov :ping_pong: :stuck_out_tongue_wink: :smiley:

view this post on Zulip Yury G. Kudryashov (Oct 06 2020 at 12:27):

Sorry, I've got distracted. I must record ~30min videos for students in the next 1h30m, then I'll come back to this.


Last updated: May 10 2021 at 08:14 UTC