Zulip Chat Archive

Stream: sphere eversion

Topic: Surrounding a point (Lemma 1.6)

Patrick Massot (Oct 08 2021 at 15:33):

The first important goal of the preliminaries in the loop chapter was to prove Lemma 1.6:

If a point lies in the convex hull of an open set $P$ , then it is surrounded by some collection of points belonging to $P$ .

Recall that in a real vector space with dimension $d$ . A point $x$ is surrounded by points $p_0, …, p_d$ if those points are affinely independent and there exist weights $w_i ∈ (0,1)$ such that $x=∑_iw_ip_i$ .

The current state is a bit messy because we have both convexity.lean and int_cvx.lean. But Oliver Nash is making really good progress on this lemma, proving refinements on Carathéodory's lemma and setting up the theory of barycentric coordinates in mathlib.

Oliver Nash (Oct 08 2021 at 15:38):

I'm very close with this now. I think #9629 is the last piece for Mathlib and within a day or so I hope to have a PR to the Sphere Eversion repo which completely proves this lemma (and tidies up the little bit of mess mentioned above).

Yaël Dillies (Oct 08 2021 at 15:52):

Thanks for this! When we were doing Sperner's lemma, we got stuck on precisely that.

Yaël Dillies (Oct 08 2021 at 15:52):

If I can be helpful for anything else, feel free to ping!

Oliver Nash (Oct 08 2021 at 17:11):

I'm done for the day so I've pushed up a branch showing work in progress: https://github.com/leanprover-community/sphere-eversion/pull/26 I'd estimate one solid day's work should close its sorry and tidy it up into something we could consider merging.

Oliver Nash (Oct 08 2021 at 17:13):

(so realistically, probably two days!)

Oliver Nash (Oct 12 2021 at 15:03):

I'm _still_ pushing on this lemma. I could go faster but I'm keen to try and do things the Right Way. The latest piece is: #9674

Eric Rodriguez (Oct 12 2021 at 15:05):

Is it possibly worth to do an LTE-like for_mathlibfolder and then focus on merging that after? Mathlib PRs are all well and good but can sometimes be slow

Oliver Nash (Oct 12 2021 at 15:06):

I think Floris has started this here but I haven't caved in just yet.

Oliver Nash (Oct 12 2021 at 15:07):

I agree it is probably necessary and it's likely I'll use this release valve to speed up my progress sooner or later.

Oliver Nash (Oct 15 2021 at 14:41):

I now have a sorry-free proof of this lemma here It needs significant tidy up (and also needs two Mathlib PRs to merge first) but it's nice to be sorry-free!

Oliver Nash (Oct 18 2021 at 12:27):

I think https://github.com/leanprover-community/sphere-eversion/pull/26 is now ready for review. Repeating a comment I made on GH, for posterity this work uses the following 31 PRs to Mathlib:

#9776 feat(linear_algebra/affine_space/independent): affine equivalences preserve affine independence of sets of points
#9747 feat(linear_algebra/affine_space/independent): add exists_affine_independent
#9727 feat(analysis/normed_space/add_torsor_bases): the convex hull has non-empty interior iff the affine span is top
#9708 feat(linear_algebra/linear_independent): add variant of exists_linear_independent
#9695 feat(linear_algebra/affine_space/affine_subspace): add lemma affine_equiv.span_eq_top_iff
#9674 feat(linear_algebra/{dimension,affine_space/finite_dimensional}): independent subsets of finite-dimensional spaces are finite.
#9657 feat(linear_algebra/affine_space/finite_dimensional): upgrade affine_independent.affine_span_eq_top_of_card_eq_finrank_add_one to an iff
#9629 feat(linear_algebra/affine_space/barycentric_coords): we can recover a point from its barycentric coordinates
#9583 feat(analysis/normed_space/add_torsor_bases): the interior of the convex hull of a finite affine basis is the set of points with strictly positive barycentric coordinates
#9564 feat(linear_algebra/affine_space/barycentric_coords): barycentric coordinates are 1 in zero dimensions
#9543 feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are open maps (in finite dimensions over a complete field)
#9540 feat(analysis/normed_space/banach): open mapping theorem for maps between affine spaces
#9538 feat(analysis/normed_space/affine_isometry): affine maps are open iff their underlying linear maps are
#9515 feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are continuous
#9508 feat(topology/basic): interior of finite intersection is intersection of interiors
#9499 feat(analysis/convex/combination): lemmas connecting convex hull with affine combinations and barycentric coordinates
#9472 feat(linear_algebra/affine_space/barycentric_coords): define barycentric coordinates
#9471 feat(topology/maps): for a continuous open map, preimage and interior commute
#9453 feat(linear_algebra/affine_space/combination): add lemma finset.map_affine_combination
#9418 feat(analysis/normed_space/add_torsor_bases): add lemma exists_subset_affine_independent_span_eq_top_of_open
#9360 feat(linear_algebra/affine_space/affine_map): add missing simp lemma affine_map.homothety_apply_same
#9113 feat(linear_algebra/affine_space/affine_subspace): prove that a set whose affine span is top cannot be empty.
#9103 feat(linear_algebra/affine_space/combination, analysis/convex/combination): basic lemmas about affine combinations, center of mass, centroid
#9070 feat(linear_algebra/affine_space/independent): homotheties preserve affine independence
#9057 feat(analysis/convex/basic): the affine image of the convex hull is the convex hull of the affine image
#9044 feat(analysis/convex/topology): add lemma convex.subset_interior_image_homothety_of_one_lt
#9005 feat(linear_algebra/affine_space/independent): affine independence is preserved by affine maps
#8983 feat(linear_algebra/affine_space/affine_equiv): affine homotheties as equivalences
#8895 feat(order/well_founded): define function.argmin, function.argmin_on
#8892 feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine
#8865 feat(algebra/big_operators/basic): add prod_dite_of_false, prod_dite_of_true

Yaël Dillies (Oct 18 2021 at 13:08):

Wow! No wonder I couldn't prove it when I needed it for Sperner's lemma.

Oliver Nash (Oct 18 2021 at 13:20):

I think only a subset of at most 10 of these are the bit you needed for that. There are also some shortcuts which, rightly or wrongly, I avoided.

Patrick Massot (Oct 18 2021 at 14:14):

This is really great. Thanks a lot for all your work on this! I'm especially happy to see that it already brought a lot of very natural things to mathlib.

Scott Morrison (Oct 18 2021 at 22:13):

It may take longer to do development this way, but the outcome is really nice!

Patrick Massot (Oct 19 2021 at 20:27):

This lemma is now officially green! The blueprint has also been updated by Oliver to explain the proof he actually formalized. One very nice thing is that the proof includes stuff that would definitely be proved on paper by drawing a small picture and nothing else, for instance this new lemma.

Last updated: Dec 20 2023 at 11:08 UTC