Lebesgue number lemma

Stream: maths

[Patrick Massot]

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]

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]

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]

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]

How would you do that?

[Reid Barton]

Look in a book on real analysis? :upside_down:

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

@Sebastien Gouezel, any thought on this topic?

[Sebastien Gouezel]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Sebastien Gouezel]

No, always in metric spaces, of course.

[Patrick Massot]

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]

what's wrong with this proof?

[Kenny Lau]

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]

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

I thought S is a subset of R^n

[Patrick Massot]

No, it's not.

[Sebastien Gouezel]

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]

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]

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

[Patrick Massot]

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

[Sebastien Gouezel]

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

[Patrick Massot]

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

[David Wärn]

Isn't that the definition?

[Patrick Massot]

No, not in this generality

[Patrick Massot]

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

[Patrick Massot]

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

[Sebastien Gouezel]

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]

Yes, I understand your plan.

[Patrick Massot]

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

[Sebastien Gouezel]

Sure!

[Patrick Massot]

I hope it could be useful for other things.

[Patrick Massot]

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

[Patrick Massot]

Cleaning up includes documenting of course.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

And Patrick even updated it to use is_countably_generated

[Patrick Massot]

I did those updates in automatic mode, without really reading...

[Patrick Massot]

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⟩ },
  by_contradiction H,
  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

[Kevin Buzzard]

If you want to make it readable, why not just add comments in between every line like I half-did here?

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Kevin Buzzard]

Oh I see! Yes this is an interesting style.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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