Stream: maths

Topic: Lebesgue number lemma

Patrick Massot (Apr 14 2020 at 20:24):

In mathlib we have a strange version of the Lebesgue number lemma which assumes compactness instead of sequential compactness. In particular it's not so useful when proving that sequentially compact subspaces of metric spaces are compact. This strange version however is derived from a version on uniform space where sequential compactness is probably not enough. My current plan is to prove a uniform space version assuming sequential compactness but also assuming the uniformity is countably generated. Does it sound good? @Reid Barton it seems you wrote those.

Patrick Massot (Apr 14 2020 at 20:25):

Is there any use of the versions of the Lebesgue assuming only compactness (provided we know that sequentially compact is equivalent to compact in metric spaces)?

Reid Barton (Apr 14 2020 at 20:40):

I don't know anything about sequential compactness. But certainly I only intended to ever apply the Lebesgue number lemma to spaces like [0, 1]^n.

Patrick Massot (Apr 14 2020 at 20:41):

Say I want to prove a subset $S$ of $\mathbb{R}^n$ is compact iff every sequence in $S$ has a converging subsequence.

Patrick Massot (Apr 14 2020 at 20:42):

How would you do that?

Reid Barton (Apr 14 2020 at 20:42):

Look in a book on real analysis? :upside_down:

Patrick Massot (Apr 14 2020 at 20:42):

The standard proof for the right to left implication using the Lebesgue number lemma.

Patrick Massot (Apr 14 2020 at 20:42):

But of course if you assume compactness in this lemma then the proof becomes less convincing.

Patrick Massot (Apr 14 2020 at 20:43):

@Sebastien Gouezel, any thought on this topic?

Sebastien Gouezel (Apr 14 2020 at 20:47):

If every sequence in S has a converging subsequence, your set is clearly closed and bounded, therefore compact :)

I agree that the classical proof goes through the Lebesgue number for sequentially compact spaces, but for me this is more of a historical curiosity (maths de classes prépa, say). I definitely used the Lebesgue number lemma for compact spaces in real maths, so the existing version is the right one for me, but probably not for teaching purposes.

Patrick Massot (Apr 14 2020 at 20:52):

Did you use it for compact spaces that are not first countable (hence may be not sequentially compact)?

Patrick Massot (Apr 14 2020 at 20:54):

I'll probably put your proof in mathlib anyway. But the classical proof is nice to formalize.

Patrick Massot (Apr 14 2020 at 20:55):

I mean it's nicely frustrating (involving discussing finite subsets).

Sebastien Gouezel (Apr 14 2020 at 21:04):

No, always in metric spaces, of course.

Patrick Massot (Apr 15 2020 at 08:11):

Sebastien Gouezel said:

If every sequence in S has a converging subsequence, your set is clearly closed and bounded, therefore compact :)

I agree that the classical proof goes through the Lebesgue number for sequentially compact spaces, but for me this is more of a historical curiosity (maths de classes prépa, say). I definitely used the Lebesgue number lemma for compact spaces in real maths, so the existing version is the right one for me, but probably not for teaching purposes.

I should really ask for a formal proof each time someone claims something about math. I was so tired yesterday night that I believed Sébastien without thinking at all. This "proof" is of course a joke.

Kenny Lau (Apr 15 2020 at 08:15):

what's wrong with this proof?

Kenny Lau (Apr 15 2020 at 08:18):

the crucial step that I^n is compact follows easily from the fact that I is compact and product of compact spaces is compact

Patrick Massot (Apr 15 2020 at 08:45):

"closed and bounded, therefore compact" is wrong (Sébastien did put a smiley after this, but I was misled by the following paragraph).

Kenny Lau (Apr 15 2020 at 08:47):

I thought S is a subset of R^n

No, it's not.

Sebastien Gouezel (Apr 15 2020 at 09:23):

In your question, S was indeed a subset of R^n, therefore the proof works. But of course it doesn't work in the generality you would like, hence the smiley.

David Wärn (Apr 15 2020 at 09:53):

I guess you can replace "closed and bounded" with "complete and totally bounded" and deduce compactness by "lion-hunting", but Lebesgue number lemma is probably easier

Sebastien Gouezel (Apr 15 2020 at 09:54):

We already have that a complete totally bounded set is compact.

Patrick Massot (Apr 15 2020 at 09:54):

Totally bounded is needed anyway. But I don't see how to get completeness.

Sebastien Gouezel (Apr 15 2020 at 09:55):

Do you already have that completeness is equivalent to the convergence of Cauchy sequences?

Patrick Massot (Apr 15 2020 at 09:56):

I didn't do that, but maybe it's already there somewhere.

David Wärn (Apr 15 2020 at 09:56):

Isn't that the definition?

Patrick Massot (Apr 15 2020 at 09:56):

No, not in this generality

Patrick Massot (Apr 15 2020 at 09:57):

We are discussing uniform spaces having a countable basis of entourages here.

Patrick Massot (Apr 15 2020 at 09:57):

So it's not the definition, but it should hold.

Sebastien Gouezel (Apr 15 2020 at 10:03):

Once you have this, start from a Cauchy sequence, say that it has a convergent subsequence, and therefore the whole sequence is converging (this last fact is already there, I know since I have used it for analytic maps)

Patrick Massot (Apr 15 2020 at 10:04):

But I'm halfway through Lebesgue number so I think I'll finish that.

Sure!

Patrick Massot (Apr 15 2020 at 10:04):

I hope it could be useful for other things.

Patrick Massot (Apr 15 2020 at 10:05):

I even hope I'll get enough motivation to do some cleanup in uniform_space.basic.

Patrick Massot (Apr 15 2020 at 10:06):

Cleaning up includes documenting of course.

Yury G. Kudryashov (Apr 15 2020 at 11:17):

We have "completeness from convergence of Cauchy sequences" near the end of cauchy.lean.

Yury G. Kudryashov (Apr 15 2020 at 11:19):

And Patrick even updated it to use is_countably_generated

Patrick Massot (Apr 15 2020 at 13:53):

Ok, I'm done with this Lebesgue number lemma. I continue to experiment with writing non-trivial proofs in a readable way. I'd like to know whether someone can read the next proof. It depends on stuff not in mathlib, but my goal is to have it readable anyway, even without tactic state, simply through the use of obtain and clear:

lemma lebesgue_number_lemma_seq [uniform_space β] {s : set β} {ι : Type*} {c : ι → set β}
(hs : seq_compact s) (hc₁ : ∀ i, is_open (c i)) (hc₂ : s ⊆ ⋃ i, c i)
(hU : is_countably_generated (𝓤 β)) :
∃ V ∈ 𝓤 β, ∀ x ∈ s, ∃ i, ball_[V] x ⊆ c i :=
begin
classical,
obtain ⟨V, hV, Vsymm⟩ :
∃ V : ℕ → set (β × β), (𝓤 β).has_antimono_basis (λ _, true) V ∧  ∀ n, swap ⁻¹' V n = V n,
from uniform_space.has_seq_basis hU, clear hU,
suffices : ∃ n, ∀ x ∈ s, ∃ i, ball_[V n] x ⊆ c i,
{ cases this with n hn,
exact ⟨V n, hV.to_has_basis.mem_of_mem trivial, hn⟩ },
obtain ⟨x, x_in, hx⟩ : ∃ x : ℕ → β, (∀ n, x n ∈ s) ∧ ∀ n i, ¬ball_[V n] x n ⊆ c i,
{ push_neg at H,
choose x hx using H,
exact ⟨x, forall_and_distrib.mp hx⟩ }, clear H,
obtain ⟨x₀, x₀_in, φ, φ_mono, hlim⟩ : ∃ (x₀ ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ (x ∘ φ ⟶ x₀),
from hs x_in, clear hs,
obtain ⟨i₀, x₀_in⟩ : ∃ i₀, x₀ ∈ c i₀,
{ rcases hc₂ x₀_in with ⟨_, ⟨i₀, rfl⟩, x₀_in_c⟩,
exact ⟨i₀, x₀_in_c⟩ }, clear hc₂,
obtain ⟨n₀, hn₀⟩ : ∃ n₀, ball_[V n₀] x₀ ⊆ c i₀,
{ have := is_open_iff_mem_nhds.mp (hc₁ i₀) _ x₀_in,
rcases (nhds_basis_uniformity hV.to_has_basis).mem_iff.mp this with ⟨n₀, _, h⟩,
use n₀,
rwa ← ball_eq_of_symmetry (Vsymm n₀) at h }, clear hc₁,
obtain ⟨W, W_in, hWW⟩ : ∃ W ∈ 𝓤 β, W ○ W ⊆ V n₀,
from comp_mem_uniformity_sets (hV.to_has_basis.mem_of_mem trivial),
obtain ⟨N, x_φ_N_in, hVNW⟩ : ∃ N, x (φ N) ∈ ball_[W] x₀ ∧ V (φ N) ⊆ W,
{ obtain ⟨N₁, h₁⟩ : ∃ N₁, ∀ n ≥ N₁, x (φ n) ∈ ball_[W] x₀,
from (tendsto_at_top' (λ (b : ℕ), (x ∘ φ) b) (𝓝 x₀)).mp hlim _ (mem_nhds_left x₀ W_in),
obtain ⟨N₂, h₂⟩ : ∃ N₂, V (φ N₂) ⊆ W,
{ rcases hV.to_has_basis.mem_iff.mp W_in with ⟨N, _, hN⟩,
use N,
exact subset.trans (hV.decreasing trivial trivial \$ nat.id_le_of_strict_mono φ_mono _) hN },
have : φ N₂ ≤ φ (max N₁ N₂),
from φ_mono.le_iff_le.mpr (le_max_right _ _),
exact ⟨max N₁ N₂, h₁ _ (le_max_left _ _), subset.trans (hV.decreasing trivial trivial this) h₂⟩ },
suffices : ball_[V (φ N)] x (φ N) ⊆ c i₀,
from hx (φ N) i₀ this,
calc
ball_[V (φ N)] x (φ N) ⊆ ball_[W] x (φ N) : preimage_mono hVNW
... ⊆ ball_[V n₀] x₀   : ball_subset_of_comp_subset x_φ_N_in hWW
... ⊆ c i₀             : hn₀,
end


Patrick Massot (Apr 15 2020 at 13:58):

My question is precisely: can those obtain serve as comments?

Patrick Massot (Apr 15 2020 at 13:59):

They give all the steps in the proof, and the clear commands flag the fact that an assumption has just being used.

Johan Commelin (Apr 15 2020 at 13:59):

I don't really know the maths, and I think I can follow what's going on quite well.

Kevin Buzzard (Apr 15 2020 at 14:00):

Oh I see! Yes this is an interesting style.

Kevin Buzzard (Apr 15 2020 at 14:01):

Yes I think this is very interesting. The obtain steps say precisely what I would be saying in my comments.

Kevin Buzzard (Apr 15 2020 at 14:02):

They also have the advantage that they name all the notation.

Reid Barton (Apr 15 2020 at 14:09):

I didn't find the clear commands particularly helpful, but where you've put them makes them easy to ignore.

Last updated: May 11 2021 at 16:22 UTC