Zulip Chat Archive

Stream: sphere eversion

Topic: exist surrounding loops

Floris van Doorn (Dec 06 2021 at 17:49):

In the proof of Lemma 1.15, ∃_surrounding_loops, how do we get the $U_i$ and the $\gamma^i$ ?
I understand that the lemma local_loops gives for each point $x \in U \setminus K$ a local family of loops, but I don't see how we get a finite family such that the domains cover $U \setminus K$ . We're not assuming that $U$ is bounded, right? The $0\le i \le N$ later in the proof suggests that we're working with a finite family. Or are we working with a countable family, and is $\gamma'$ some kind of limit?

Floris van Doorn (Dec 06 2021 at 18:51):

Thinking about it more, we do need a countably infinite sequence. And by Cor 1.14, the sequence is locally eventually constant (each $x$ has a neigborhood $U$ such that the sequence $n\mapsto \gamma_n'|_U$ is eventually constant, where $\gamma_n'$ are the successive stages of $\gamma'$ ), so taking the limit shouldn't be too hard.

Patrick Massot (Dec 06 2021 at 19:02):

I'm sorry there is a typo in that proof "a local finite covering" doesn't mean anything, I meant to write "a locally finite covering".

Patrick Massot (Dec 06 2021 at 19:05):

I don't know why I wrote this $N$ . Indeed this is all meant to give rise to a sequence which, at any given point, is ultimately constant hence trivially (on paper, maybe not in Lean...) converging.

Floris van Doorn (Dec 06 2021 at 19:05):

Makes sense. Where in the argument do you need the fact that the covering is locally finite?

Patrick Massot (Dec 06 2021 at 19:10):

The actual reason is we always write this without thinking about it. The technical reason is probably that we first argue there is a locally finite cover before arguing we can get a countable cover.

Floris van Doorn (Dec 06 2021 at 19:13):

Ok, fair. I think this proof doesn't need it, so I'll try using docs#topological_space.countable_cover_nhds_within.

Patrick Massot (Dec 06 2021 at 19:16):

Great! One good side of formal mathematics is that whoever proves the lemma is the winner in any argument about what is needed in the proof.

Floris van Doorn (Dec 07 2021 at 11:24):

Thinking about it more, the locally finiteness does seem needed. If every neighborhood of $x$ intersects infinitely many sets, then I think $\gamma'$ might be discontinuous at $x$ : at every stage we get the guarantee that we don't change $\gamma'_n$ around a neighborhood of $x$ , but these neighborhoods might be shrinking, and the intersection of all of them need not be a neighborhood of $x$ .

Patrick Massot (Dec 14 2021 at 18:13):

Note for contributors: Floris is currently distracted by Lean 4 meta-programming so don't hesitate to contribute if you like covering lemmas. There is a candidate lemma here which is hopefully enough, together with a proof strategy.

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

This lemma is meant to cover up the bluff in this paper proof.

Patrick Massot (Dec 14 2021 at 18:15):

@Yury G. Kudryashov this is a good opportunity to contribute if you want, since you wrote all the paracompact stuff.

Yury G. Kudryashov (Dec 14 2021 at 18:19):

Could you please point me to the lemma we want to prove and the lemma we want to use in the proof?

Patrick Massot (Dec 14 2021 at 18:21):

The actual target is here (except there is a $N$ which should be $+\infty$ ) and the candidate technical lemma independent of the project is here.

Yury G. Kudryashov (Dec 14 2021 at 18:59):

I'll have a look tonight or tomorrow.

Floris van Doorn (Dec 14 2021 at 21:53):

I indeed didn't have time to look at this yet today.

I looked at it a bit now, and this was indeed the step I was stuck on.

Two minor comments:

I think in the proof you first want to get a sequence u and v indexed by some docs#encodable type (as a union/sigma of countably many finite types), and as a separate step change the encodable type to nat.
To do the last step (encodable ~> nat) you can use docs#encodable.decode₂, but you need a default "junk" value for your u and v. For this I think you need an minor additional assumption (either [nonempty X] or P \empty)

Floris van Doorn (Dec 14 2021 at 21:54):

It would be great if you can look at this Yury!

Patrick Massot (Dec 14 2021 at 21:55):

I'd be willing to assume P \empty, but I guess we can also start with a case disjunction (hopefully the statement holds for the empty space).

Yury G. Kudryashov (Dec 15 2021 at 19:37):

I suggest the following:

Modify docs#refinement_of_locally_compact_sigma_compact_of_nhds_basis_set so that it outputs an encodable type (done locally, I'll PR later tonight).
Use it to get a locally finite covering by open sets v a such that P (v a) and each closure (v a) is compact.
Use the shrinking lemma (we can do it because a paracompact t2 space is normal) to get a refinement u a such that closure (u a) ⊆ v a.
Use the embedding of the index type to nat coming from [encodable] to get a family indexed by natural numbers (we need either nonempty X or P \empty for this step).

Floris van Doorn (Dec 15 2021 at 20:42):

We talked about using the shrinking lemma. We concluded that using the shrinking lemma directly didn't work, because we want the v's to be locally finite and the us to cover the space. But maybe you have an idea that we missed.

Floris van Doorn (Dec 15 2021 at 20:44):

The shrinking lemma gives only that the us are locally finite.

Yury G. Kudryashov (Dec 15 2021 at 20:47):

docs#exists_Union_eq_closed_subset

Yury G. Kudryashov (Dec 15 2021 at 20:47):

If you start with a covering by v i such that closure (v i) is compact, then the new u i will be compact as well and they will cover the space.

Yury G. Kudryashov (Dec 15 2021 at 21:04):

UPD: you don't need to modify docs#refinement_of_locally_compact_sigma_compact_of_nhds_basis_set because we have docs#locally_finite.countable_of_sigma_compact

Floris van Doorn (Dec 15 2021 at 21:20):

You're right. I misremembered the problem.

I think the problem is that @Patrick Massot's lemma is not actually the one we want, we want something slightly different (sorry!).
We are really interested in the case where everything is restricted to some given open set V, except that the compactness of u has to hold in X, not in V. So this:

import topology.paracompact

open set
open_locale topological_space

variables {X : Type*} [topological_space X] [locally_compact_space X] [sigma_compact_space X]
  [t2_space X] {V : set X} (hV : is_open V)

lemma foo {P : set V → Prop} (hP : antitone P) (hX : ∀ x : V, ∃ U ∈ 𝓝 x, P U) (h0 : P ∅) :
∃ (u : ℕ → set X) (v : ℕ → set X), ∀ n,
  is_compact (u n) ∧ is_open (v n) ∧ P (coe ⁻¹' v n) ∧
  u n ⊆ v n ∧ v n ⊆ V ∧ locally_finite v ∧ V ⊆ ⋃ n, u n :=
sorry

Applying Patrick's foo to V gives you almost everything, except only that u n is compact in V, but it might not be compact (or even closed) in X.
Patrick, do you agree that this is the version we want?

Floris van Doorn (Dec 15 2021 at 21:24):

Note: to get countability in a previous attempt, I used docs#topological_space.countable_cover_nhds_within. (We also know [second_countable X], if needed.)

Yury G. Kudryashov (Dec 15 2021 at 21:40):

You get countability from locally_finite for free, see above.

Yury G. Kudryashov (Dec 15 2021 at 21:42):

I'll have a look later tonight.

Patrick Massot (Dec 15 2021 at 22:26):

Unfortunately I have very little time tonight. But I don't understand Floris's objection. If u n is compact in V then it's compact in X. The inclusion of V into X is continuous hence it maps compact sets to compact sets.

Floris van Doorn (Dec 16 2021 at 00:09):

Now I'm not sure if my objection holds anymore.

So we restrict our attention to V and ignore X, in step (2) we get v a with closure (v a) compact, and then the shrinking lemma gives you u i such that closure (u i) ⊆ v i. This means that closure (u i) will be compact, since it is a closed subset of a compact set.
From the perspective of X, we know that coe '' closure (v a) is compact, hence closed, so closure (coe '' v a) = coe '' closure (v a) is also compact. Similarly, closure (u a) is compact (in V), hence closure (coe '' u a) is compact (in X).

Ok, so I now think again that applying the shrinking lemma will work.
I thought earlier that it wouldn't suffice, because I forgot to take into account (in an intermediate lemma) that we're working with compact sets in V not just closed sets (where we would have a problem that being closed in V is weaker than being closed in X).

Yury G. Kudryashov (Dec 16 2021 at 06:35):

Can you prove [sigma_compact_space V]?

Yury G. Kudryashov (Dec 16 2021 at 12:13):

Could you please explain what are X, V, and P in the actual proof?

Yury G. Kudryashov (Dec 16 2021 at 12:14):

I mean, in the proof where you're going to apply this lemma.

Floris van Doorn (Dec 16 2021 at 12:40):

We're applying this lemma foo in Lemma 1.15 of the blueprint. The X is foo is E in the blueprint, V is $U \setminus \overline{U_0'}$ and P(O) means "there is a family of loops in $\mathcal{L}(g,\beta,O,\Omega)$ "(defined in Def 1.11, and we know that this locally holds by Lemma 1.12)

Floris van Doorn (Dec 16 2021 at 12:41):

I think we know that V is $\sigma$ -compact, but type-class inference will not find it automatically...

Floris van Doorn (Dec 16 2021 at 12:42):

Is an open subset of a finite dimensional vector space over $\mathbb{R}$ $\sigma$ -compact?

Floris van Doorn (Dec 16 2021 at 12:48):

Yes it is, if we use the fact that open and closed sets in a locally compact Hausdorff space is again locally compact. I cannot find this fact in mathlib though (it cannot be an instance, but does it exist as a lemma?).

Yury G. Kudryashov (Dec 16 2021 at 12:55):

I'm going to add open_embedding.locally_compact and closed_embedding.locally_compact.

Yury G. Kudryashov (Dec 16 2021 at 12:55):

(unless you're already working on these)

Floris van Doorn (Dec 16 2021 at 13:06):

I am not currently working on this.

Floris van Doorn (Dec 16 2021 at 13:08):

I think it would also be useful to specialize them to is_open.subtype_locally_compact_space and is_closed.subtype_locally_compact_space (that might be something people look for, like I did)

Yury G. Kudryashov (Dec 16 2021 at 13:11):

Sure.

Yury G. Kudryashov (Dec 16 2021 at 15:05):

#10844

Floris van Doorn (Jan 10 2022 at 18:41):

I'm getting back to this.
I think Patrick's foo (where we the neighborhoods satisfying P around all x) is not quite sufficient to get my formulation of foo (where we have the neighborhoods satisfying P only for x in some open set V).
Applying Patrick's foo to V gives us most of the things, but we get the locally finiteness of v only for x ∈ V. This means that the vs in my formulation might not be locally finite around points on the boundary of V.
This will be problematic if we want the γin the conclusion of exists_surrounding_loops to be continuous globally (not just in the U of that theorem).
To get my version of foo, we probably have to follow Patrick's proof strategy, unless I'm missing something again.

Floris van Doorn (Jan 12 2022 at 16:57):

I just pushed a proof of Lemma 1.16 (previously 1.15), where the only sorry is (my formulation of) foo above.
The rest of the proof was still quite tricky: constructing the sequence of loops, proving that they were locally eventually constant, constructing the limit, and proving all the properties of the limit. In the end I wrote a small library for eventually constant and locally eventually constant sequences (w.r.t. an arbitrary filter).
I also made some changes that are relevant for the blueprint (I will update the blueprint once the whole proof is finished):

In the lemma extend_loops I added the condition that $\gamma$ equals $\gamma_0$ (also) near the complement $U_1^c$ : this allows for much more control of the behavior of $\gamma$ and allows us to show that the $\gamma^i$ are locally eventually constant on all points (also outside $U$ ).
In the proof of Lemma 1.16 it is fine if the $U_i$ cover all of $U$ , we can remove mentioning $U_0'$ from the proof. Then we can still conclude that $\gamma'$ coincides with $\gamma$ near $K$ : since the $\gamma^i$ are locally eventually constant and $K$ is compact, we can conclude that $\gamma^i$ is eventually constant on some neighborhood of $K$ .

Patrick Massot (Jan 12 2022 at 17:24):

This sounds wonderful! I missed your previous message in this thread. I'll try to understand what you wrote.

Oliver Nash (Jan 12 2022 at 17:56):

Nice work Floris!

I've been taking a break from Sphere Eversion for the last month or so but I plan to resume in about a week after I finish some other bits and pieces. I'll probably start attacking the reparameterisation lemma.

Floris van Doorn (Jan 13 2022 at 09:43):

I think my formulation of foo is false: it is possible that for x on the boundary of V there is no neighborhood O around x where P O holds. In that case, it is impossible to choose the v in the conclusion so that it is locally finite around x.
@Patrick Massot I'll come by your office this afternoon, maybe we can discuss possible solutions.

Patrick Massot (Jan 13 2022 at 10:02):

I'm got going to Orsay this week because of my arm. Because my accident has been declared as a work accident and I was ordered to stop working for one week, I can't go to my office. If I have another accident there then the administrative situation would become a nightmare.

Patrick Massot (Jan 13 2022 at 10:03):

But we can have a video call.

Patrick Massot (Jan 13 2022 at 10:03):

I'll think about this lemma in the beginning of the afternoon

Floris van Doorn (Jan 13 2022 at 10:39):

Oh I see. I hope your arm is recovering well, though!

Floris van Doorn (Jan 13 2022 at 10:52):

I see two possibilities:

In the conclusion of exists_surrounding_loops change the everywhere continuity of $\gamma$ to the continuity of $\gamma$ on $U$ (this would mean I'm taking back the Christmas present I gave you :big_smile: )
Strengthen the conditions of exists_surrounding_loops so that we can get the continuity conclusion everywhere, for example by requiring all conditions on the closure of $U$ (in which case we can reformulate it using a closed set). But that is probably not okay for the situations in which we apply this lemma, though.

Patrick Massot (Jan 13 2022 at 14:43):

Indeed there is no way foo2 can be true.

Patrick Massot (Jan 13 2022 at 14:44):

I think we could strengthen the conditions by requiring them on the closure of U (I don't want to give my Christmas present).

Floris van Doorn (Jan 13 2022 at 14:47):

If you're quite confident that this will not cause issues, I can make those changes.
If you're unsure, we can also keep this on hold for now and continue with the dependencies, and see what exactly we need.

Patrick Massot (Jan 13 2022 at 14:48):

We won't use the loop family near the boundary of U anyway.

Patrick Massot (Jan 13 2022 at 14:50):

In proposition 1.3, the average value condition will only be used on a compact set contained in U

Patrick Massot (Jan 13 2022 at 15:39):

Maybe the reparametrization lemma will become harder to state if we change that. It's pretty difficult to make sure everything will fit without trying. It would be an interesting problem if this wasn't entirely a formalization artifact (on paper nothing exists outside U).

Patrick Massot (Jan 13 2022 at 15:40):

It means I need to work more on the applications of Chapter 1 in Chapter 2. But everything is even slower than usual with a single arm.

Patrick Massot (Jan 13 2022 at 16:09):

@Floris van Doorn I'm pretty we can assume that $g$ and $\beta$ are smooth on a neighborhood of $\overline{U}$ in Proposition 1.3.

Floris van Doorn (Jan 17 2022 at 18:19):

With these modifications I finished exists_surrounding_loops.
The new statement is below. Note that the C in the formulation below is the closure of U in the blueprint and U' is any open neighborhood of C.

lemma exists_surrounding_loops [finite_dimensional ℝ F] {C U' : set E}
  (hK : is_compact K) (hC : is_closed C) (hU' : is_open U') (hCU' : C ⊆ U')
  (hΩ_op : is_open (Ω ∩ fst ⁻¹' U'))
  (hΩ_conn : ∀ x ∈ C, is_connected (prod.mk x ⁻¹' Ω))
  (hg : ∀ x ∈ C, continuous_at g x) (hb : continuous b)
  (hb_in : ∀ x ∈ C, (x, b x) ∈ Ω)
  (hconv : ∀ x ∈ C, g x ∈ convex_hull ℝ (prod.mk x ⁻¹' Ω))
  {γ₀ :  E → ℝ → loop F}
  (hγ₀_surr : ∃ V ∈ 𝓝ˢ K, surrounding_family_in g b γ₀ V Ω) :
  ∃ γ : E → ℝ → loop F, surrounding_family_in g b γ C Ω ∧ ∀ᶠ x in 𝓝ˢ K, γ x = γ₀ x

Patrick Massot (Jan 17 2022 at 18:25):

Great!

Patrick Massot (Jan 17 2022 at 18:25):

Congratulations!

Oliver Nash (Jan 17 2022 at 21:58):

Congratulations indeed, this is superb!

Oliver Nash (Jan 17 2022 at 21:58):

I'm feeling guilty because I've succumbed to the temptation to do a bit more Lie theory but I plan to dive back into Sphere Eversion within days.

Oliver Nash (Feb 14 2022 at 14:21):

I resumed work on Sphere Eversion this morning. Am I right in thinking that thanks to Floris we can turn exists_surrounding_loops green as soon as we fill in this sorry times_cont_diff_clm_apply ?

Oliver Nash (Feb 14 2022 at 14:21):

Should I go ahead and do this?

Patrick Massot (Feb 14 2022 at 14:35):

Yes, please

Oliver Nash (Feb 14 2022 at 21:28):

I've just opened https://github.com/leanprover-community/sphere-eversion/pull/49 which closes this sorry.

Oliver Nash (Feb 14 2022 at 21:30):

I'll spend a bit more time on this again tomorrow, partly as the code could do with some work but mostly because I'm not too happy that I introduced another finite-dimensionality assumption. Still, it's another sorry squashed!

Patrick Massot (Feb 14 2022 at 21:42):

I didn't spend too much time thinking about this lemma. Is it true in infinite dimension?

Oliver Nash (Feb 14 2022 at 21:46):

I don’t know! I didn’t think hard about it yet.

Oliver Nash (Feb 15 2022 at 14:50):

I thought about it and the finite-dimensionality I added was not required. I've just updated the PR so that it no longer requires this hypothesis. It still uses another possibly-redundant finite-dimensionality assumption (which I did not introduce) but I think this isn't worth worrying about.

Patrick Massot (Feb 15 2022 at 15:19):

Nice! Do you still want to work on this PR or is it ok?

Oliver Nash (Feb 15 2022 at 15:32):

I've just finished messing with it.

Patrick Massot (Feb 15 2022 at 16:03):

Thanks!

Oliver Nash (Feb 15 2022 at 17:57):

I've just pushed https://github.com/leanprover-community/sphere-eversion/pull/50 which nukes some more trivial sorrys rendering loops/surrounding.lean now sorry-free.

Patrick Massot (Feb 15 2022 at 18:19):

And #print axioms exists_surrounding_loop confirms!

Oliver Nash (Feb 22 2022 at 18:43):

For some reason this lemma has turned blue again here: https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph.html

Patrick Massot (Feb 22 2022 at 19:10):

We really need to find time to switch to building the blueprint during CI.

Patrick Massot (Feb 22 2022 at 19:13):

The reason why this lemma turned blue is not very interesting (it's a side effect of splitting the LTE blueprint into two parts), but this wouldn't have been an issue with a CI build instead of local build and pushing the built files.

Last updated: Dec 20 2023 at 11:08 UTC