Sphere eversion project

Stream: maths

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

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]

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

[Patrick Massot]

Proof ready to be formalized

[Johan Commelin]

Aha

[Johan Commelin]

As in: all dependencies are green?

[Patrick Massot]

It means everything the proof depends on has been formalized.

[Patrick Massot]

Yes

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

PR!

[Kevin Buzzard]

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

[Sebastien Gouezel]

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

[Patrick Massot]

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

[Patrick Massot]

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]

When can I do sep#corrugation?

[Johan Commelin]

sphere#1

[Kevin Buzzard]

That's a good start

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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.

[Johan Commelin]

image.png

[Johan Commelin]

This is what the website looks like on a small screen

[Johan Commelin]

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

[Patrick Massot]

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.

[Johan Commelin]

sphere#2

[Bhavik Mehta]

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]

@Bhavik Mehta were you working on a mathlib branch?

[Bhavik Mehta]

No

[James Arthur]

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]

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

[Scott Morrison]

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)

[Scott Morrison]

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

[Scott Morrison]

@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]

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

[Bhavik Mehta]

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

[Scott Morrison]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Scott Morrison]

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]

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]

@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]

which hence lead me away from using indices.

[Scott Morrison]

(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]

I was thinking about something involving an actual center_mass.

[Yury G. Kudryashov]

But probably your version is better.

[Yury G. Kudryashov]

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

[Scott Morrison]

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]

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]

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]

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

[Jalex Stark]

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

[Johan Commelin]

@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

[Jalex Stark]

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]

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]

@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]

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]

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

[Johan Commelin]

Also... a README

[Scott Morrison]

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]

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]

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

[Jalex Stark]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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]

It's next stop Hacker News remember.

[Kevin Buzzard]

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

[Kevin Buzzard]

We have to be ready

[Jalex Stark]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Jalex Stark]

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]

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

[Scott Morrison]

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]

2. 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]

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]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

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

[Yury G. Kudryashov]

#2956

[Johan Commelin]

Yury G. Kudryashov said:

#2956

It's on the merge queue already

[Patrick Massot]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I am still interested in a top-down approach.

[Mario Carneiro]

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

[Kevin Buzzard]

We are making a plan Mario

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

It is

[Kevin Buzzard]

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]

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

[Patrick Massot]

Oh yes I hope it is.

[Mario Carneiro]

Right, it's like groundbreaking in a construction project

[Mario Carneiro]

you have the blueprint, now you need the physical scaffolding

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Patrick's project just opens more doors I think.

[Patrick Massot]

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]

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

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

[Kyle Miller]

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]

@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]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

mathematical deathmatch!

[Kevin Buzzard]

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]

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

[Jalex Stark]

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]

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

[Patrick Massot]

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

[Bhavik Mehta]

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]

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]

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]

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

[Patrick Massot]

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]

@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]

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.

[Johan Commelin]

Aha. Thanks.

[Patrick Massot]

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

[Johan Commelin]

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]

@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]

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

[Scott Morrison]

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]

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]

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.

[Patrick Massot]

Thanks Scott!

[Patrick Massot]

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]

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]

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]

@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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

#2981

[Yury G. Kudryashov]

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]

@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]

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]

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]

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

[Johan Commelin]

I think I have a slight preference for not squashing.

[Scott Morrison]

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

[Joseph Myers]

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)

[Scott Morrison]

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]

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]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

Is there a maths proof somewhere for Lemma 2.13?

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

I could easily save a couple of clicks here.

[Jalex Stark]

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

[Patrick Massot]

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]

@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]

Great, Bhavik opened a WIP PR.

[Bhavik Mehta]

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]

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]

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]

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

[Patrick Massot]

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

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Patrick Massot]

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

[Patrick Massot]

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]

An approach was already explored in #1160.

[Sebastien Gouezel]

See in particular the comments by Reid there.

[Patrick Massot]

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

[Patrick Massot]

@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]

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]

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]

Did you try to prove transitivity?

[Patrick Massot]

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

[Bhavik Mehta]

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]

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

[Patrick Massot]

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

[Sebastien Gouezel]

Again, all this is already done in #1160.

[Patrick Massot]

@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]

Wonderful, looks great, thanks!

[Reid Barton]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

It doesn't look easier though.

[Bhavik Mehta]

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

[Bhavik Mehta]

As far as I can tell

[Reid Barton]

Yes, use the subspace topology.

[Reid Barton]

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]

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]

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]

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

[Johan Commelin]

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

[Jean Lo]

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]

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]

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

[Johan Commelin]

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]

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]

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

[Yury G. Kudryashov]

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]

Oh I have a proof of the commute statement.

[Patrick Massot]

My last 5 PRs or so are working towards this.

[Patrick Massot]

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

[Patrick Massot]

Do you want to see the proof?

[Patrick Massot]

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]

What induction principle are you talking about?

[Yury G. Kudryashov]

Found #3978

[Yury G. Kudryashov]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Yury G. Kudryashov]

Thank you!

[Patrick Massot]

Is that version suitable for your use?

[Yury G. Kudryashov]

Most probably yes but there may be difficulties.

[Yury G. Kudryashov]

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

[Patrick Massot]

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?

[Patrick Massot]

I opened #4167

[Yury G. Kudryashov]

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.

[Patrick Massot]

Very nice!

[Patrick Massot]

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]

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]

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]

Yes, I'll reopen the pr tomorrow

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Oliver Nash]

Having only just discovered this thread I'm going to use it to advertise #8892

[Patrick Massot]

The sphere eversion project is moving again. I got distracted by the liquid tensor experiment but I now want to come back to it. Recently I got a lot of help from Oliver Nash, and Floris van Doorn seems to be interested as well. Inspired by the efficient organization of LTE, I just created a new stream #sphere eversion instead of trying to fit everything into a single topic. Future updates will be posted there. I'll start writing messages describing the current state and entry points of the project.

[Patrick Massot]

I am very pleased to announce the full completion of the sphere eversion project! As planned, we formalized Smale's sphere eversion theorem as a consequence of a much more abstract and general theorem by Gromov. The goal was to prove that proof assistants are not limited to algebra and elementary analysis but can do differential geometry as well. The main team was made of Floris van Doorn, Oliver Nash and myself. But of course we built on the amazing work of the whole Lean community that brought us Lean and mathlib.

This project was first mentioned as a dream during the FoMM2020 meeting in Pittsburgh and I started to work on an informal blueprint sometime around May 2020, but the project really took off one year ago when I was joined by Oliver and Floris.

[Riccardo Brasca]

Congratulations!!

[Patrick Massot]

It is tricky to start listing other names from the community because mathlib is really a massive collaboration. But if we exclude very foundational things like general topology and linear algebra then I think it's safe to mention that the project relies particularly on the work of Yury Kudryashov and Sébastien Gouëzel on differential calculus and integration and of Sébastien Gouëzel and Heather Macbeth on differentiable manifolds. Particularly related to the project title, Heather gave us a sphere (as a differentiable manifold) to turn inside out, as well as rotations to use in the process.

[Johan Commelin]

Proficiat @Patrick Massot @Floris van Doorn @Oliver Nash ! A true milestone!

[Filippo A. E. Nuccio]

Am I wrong or the project does not appear in the dedicated page on the community website?

[Yaël Dillies]

No it does not. That was reported a few weeks ago already.

[Patrick Massot]

https://github.com/leanprover-contrib/leanprover-contrib/actions/runs/3175159229/jobs/5172851813 :sad:

[Patrick Massot]

https://github.com/leanprover-contrib/leanprover-contrib/actions suggests there is a real problem and it's not new

[Yaël Dillies]

Wait, the workflow broke precisely when Floris added sphere-eversion to the list of projects.

[Eric Wieser]

Annoyingly I now get an email every time that job fails!

[Eric Wieser]

I would guess that we need to split the CI up into one job per project

[Eric Wieser]

From the github docs:

• Job execution time - Each job in a workflow can run for up to 6 hours of execution time. If a job reaches this limit, the job is terminated and fails to complete.
• Workflow run time - Each workflow run is limited to 35 days. If a workflow run reaches this limit, the workflow run is cancelled. This period includes execution duration, and time spent on waiting and approval.

So we have plenty of headroom if we can distribute the work

[Eric Wieser]

Oh, I think the problem here is that the CI is incremental

[Eric Wieser]

I'll see if I can parallelize the different lean versions

[Eric Wieser]

Attempted in https://github.com/eric-wieser/leanprover-contrib/actions/runs/3510677680

[Floris van Doorn]

Building the project took only 5-20 minutes before I added the two new projects. Why does it suddenly need 6 hours?

[Eric Wieser]

Because it had to build it for every lean version

[Eric Wieser]

Splitting the build did the trick, I'll try to clean up the mess I've made of the script

[Floris van Doorn]

I see. And once it succeeds, it will just use the cache next time?

[Eric Wieser]

Yes

[Eric Wieser]

But every time a new lean version or a new project was added, it would previously get overloaded

[Eric Wieser]

PR at https://github.com/leanprover-contrib/leanprover-contrib/pull/22

[Notification Bot]

18 messages were moved from this topic to #general > Sphere eversion project not appearing in project list by Eric Wieser.