## Stream: maths

### Topic: Sphere eversion project

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

#### Bhavik Mehta (Jun 03 2020 at 16:06):

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

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

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

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

#### Johan Commelin (Jun 03 2020 at 16:16):

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

Aha

#### Johan Commelin (Jun 03 2020 at 16:16):

As in: all dependencies are green?

#### Patrick Massot (Jun 03 2020 at 16:16):

It means everything the proof depends on has been formalized.

Yes

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

#### Johan Commelin (Jun 03 2020 at 16:18):

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

PR!

#### Kevin Buzzard (Jun 03 2020 at 16:20):

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

#### Sebastien Gouezel (Jun 03 2020 at 16:20):

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

#### Patrick Massot (Jun 03 2020 at 16:21):

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

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

#### Kevin Buzzard (Jun 03 2020 at 16:24):

When can I do sep#corrugation?

sphere#1

#### Kevin Buzzard (Jun 03 2020 at 16:26):

That's a good start

#### Johan Commelin (Jun 03 2020 at 16:26):

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

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

#### Patrick Massot (Jun 03 2020 at 16:34):

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

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

#### Johan Commelin (Jun 03 2020 at 16:36):

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

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

image.png

#### Johan Commelin (Jun 03 2020 at 16:37):

This is what the website looks like on a small screen

#### Johan Commelin (Jun 03 2020 at 16:38):

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

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

sphere#2

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

#### Johan Commelin (Jun 03 2020 at 18:41):

@Bhavik Mehta were you working on a mathlib branch?

No

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

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

#### Scott Morrison (Jun 03 2020 at 23:18):

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

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

#### Scott Morrison (Jun 03 2020 at 23:18):

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

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

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

#### Bhavik Mehta (Jun 04 2020 at 02:14):

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

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

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

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

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

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

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

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

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

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


#### Scott Morrison (Jun 04 2020 at 04:12):

which hence lead me away from using indices.

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

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

I was thinking about something involving an actual center_mass.

#### Yury G. Kudryashov (Jun 04 2020 at 04:18):

But probably your version is better.

#### Yury G. Kudryashov (Jun 04 2020 at 04:18):

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

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

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


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

#### Kevin Buzzard (Jun 04 2020 at 07:58):

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

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

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

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

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

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

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

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


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

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

#### Jalex Stark (Jun 04 2020 at 08:14):

sphere-eversion#4

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

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

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

#### Kevin Buzzard (Jun 04 2020 at 08:16):

It's next stop Hacker News remember.

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

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

#### Jalex Stark (Jun 04 2020 at 08:18):

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

#### Johan Commelin (Jun 04 2020 at 08:20):

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

#### Johan Commelin (Jun 04 2020 at 08:21):

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

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

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

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

#### Kevin Buzzard (Jun 04 2020 at 08:25):

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

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


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

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

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


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

#### Jalex Stark (Jun 04 2020 at 08:36):

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

#### Jalex Stark (Jun 04 2020 at 08:36):

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

#### 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.")

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

#2956

#### Johan Commelin (Jun 05 2020 at 04:55):

Yury G. Kudryashov said:

#2956

It's on the merge queue already

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:21):

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

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

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

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

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

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

#### Patrick Massot (Jun 05 2020 at 08:25):

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

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

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

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:31):

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:33):

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:34):

I am still interested in a top-down approach.

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

#### Kevin Buzzard (Jun 05 2020 at 08:35):

We are making a plan Mario

#### Patrick Massot (Jun 05 2020 at 08:35):

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

#### Mario Carneiro (Jun 05 2020 at 08:35):

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

It is

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

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

#### Patrick Massot (Jun 05 2020 at 08:36):

Oh yes I hope it is.

#### Mario Carneiro (Jun 05 2020 at 08:36):

Right, it's like groundbreaking in a construction project

#### Mario Carneiro (Jun 05 2020 at 08:36):

you have the blueprint, now you need the physical scaffolding

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

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:39):

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:40):

Patrick's project just opens more doors I think.

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

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

#### Kevin Buzzard (Jun 05 2020 at 08:55):

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

#### 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:X \to Y$ is a smooth function whose differential $df:TX\to TY$ is everywhere injective. "Deformations" refers to smooth homotopies through the space of immersions, i.e. smooth maps $F: [0,1]\times X\to Y$ such that $f_t(x)=F(t,x)$ is an immersion for each $t$. Such homotopies are known as regular homotopies.)

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

#### Patrick Massot (Jun 05 2020 at 10:47):

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

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

#### Patrick Massot (Jun 05 2020 at 10:49):

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

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

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

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

#### Scott Morrison (Jun 05 2020 at 11:08):

mathematical deathmatch!

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

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

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

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

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

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

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

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

#### Yury G. Kudryashov (Jun 05 2020 at 16:58):

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

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

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

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

Aha. Thanks.

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

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

#### 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. :-)

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

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

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

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

Thanks Scott!

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

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

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

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

#### Patrick Massot (Jun 07 2020 at 19:02):

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

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

#2981

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

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

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

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

#### Patrick Massot (Jun 08 2020 at 08:57):

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

#### Johan Commelin (Jun 08 2020 at 08:58):

I think I have a slight preference for not squashing.

#### Scott Morrison (Jun 08 2020 at 09:24):

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

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

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)


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

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

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

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

#### Johan Commelin (Jun 10 2020 at 18:22):

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

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

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


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

#### Bhavik Mehta (Jun 26 2020 at 15:41):

Is there a maths proof somewhere for Lemma 2.13?

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

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

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

#### Patrick Massot (Jun 26 2020 at 15:49):

I could easily save a couple of clicks here.

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

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

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

#### Patrick Massot (Jun 26 2020 at 18:13):

Great, Bhavik opened a WIP PR.

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

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

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

#### Patrick Massot (Jun 26 2020 at 18:28):

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

#### Patrick Massot (Jun 26 2020 at 18:29):

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

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

#### Bhavik Mehta (Jun 26 2020 at 18:30):

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

#### Bhavik Mehta (Jun 26 2020 at 18:34):

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

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

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

#### Sebastien Gouezel (Jun 26 2020 at 19:59):

An approach was already explored in #1160.

#### Sebastien Gouezel (Jun 26 2020 at 20:00):

See in particular the comments by Reid there.

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

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

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

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

#### Patrick Massot (Jun 29 2020 at 15:57):

Did you try to prove transitivity?

#### Patrick Massot (Jun 29 2020 at 15:58):

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

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

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

#### Patrick Massot (Jun 29 2020 at 16:02):

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

#### Sebastien Gouezel (Jun 29 2020 at 16:07):

Again, all this is already done in #1160.

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

#### Bhavik Mehta (Jul 01 2020 at 16:21):

Wonderful, looks great, thanks!

#### Reid Barton (Jul 01 2020 at 16:23):

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

#### Reid Barton (Jul 01 2020 at 16:24):

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

#### Bhavik Mehta (Jul 01 2020 at 16:24):

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

#### Reid Barton (Jul 01 2020 at 16:24):

It doesn't look easier though.

#### Bhavik Mehta (Jul 01 2020 at 16:25):

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

#### Bhavik Mehta (Jul 01 2020 at 16:25):

As far as I can tell

#### Reid Barton (Jul 01 2020 at 16:25):

Yes, use the subspace topology.

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

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

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

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

#### Johan Commelin (Jul 04 2020 at 06:31):

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

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

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

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

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

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

#### Patrick Massot (Aug 27 2020 at 19:03):

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

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

#### Patrick Massot (Sep 15 2020 at 20:17):

Oh I have a proof of the commute statement.

#### Patrick Massot (Sep 15 2020 at 20:17):

My last 5 PRs or so are working towards this.

#### Patrick Massot (Sep 15 2020 at 20:18):

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

#### Patrick Massot (Sep 15 2020 at 20:19):

Do you want to see the proof?

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

#### Yury G. Kudryashov (Sep 15 2020 at 20:43):

What induction principle are you talking about?

Found #3978

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

#### 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 ∂μ)


#### Patrick Massot (Sep 15 2020 at 21:00):

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

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


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

Thank you!

#### Patrick Massot (Sep 15 2020 at 21:14):

Is that version suitable for your use?

#### Yury G. Kudryashov (Sep 15 2020 at 21:32):

Most probably yes but there may be difficulties.

#### Yury G. Kudryashov (Sep 15 2020 at 21:34):

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

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

I opened #4167

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

Very nice!

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

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

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

#### Yury G. Kudryashov (Sep 25 2020 at 18:30):

Yes, I'll reopen the pr tomorrow

#### Johan Commelin (Oct 06 2020 at 12:25):

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

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