First Baire theorem

Stream: mathlib4

[Snir Broshi]

The module docstring of Mathlib/Topology/Baire/CompleteMetrizable.lean says:

/-!
# First Baire theorem

In this file we prove that a completely metrizable topological space is a Baire space.
Since `Mathlib` does not have the notion of a completely metrizable topological space yet,
we state it for a complete uniform space with countably generated uniformity filter.
-/

This comment is from #10648 in March 2024, which also changed the hypothesis from [PseudoEMetricSpace X] [CompleteSpace X] to [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated].
A year later, #22926 added docs#TopologicalSpace.IsCompletelyMetrizableSpace.

It seems that now that we have completely metrizable spaces we should use them in docs#BaireSpace.of_pseudoEMetricSpace_completeSpace.

I'm not used to these definitions yet (just ran across this comment) so I'm not sure which of the 3 options is more general / preferred:

• [PseudoEMetricSpace X] [CompleteSpace X] (previous)
• [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated] (current)
• [TopologicalSpace X] [IsCompletelyMetrizableSpace X] (now possible)

In any case the docstring should be changed. wdyt?

[Yury G. Kudryashov]

While these properties are all equivalent in some sense, they require different canonical structures on X, with the last one having weakest assumptions.

[Yury G. Kudryashov]

So, we should use the last one in assumptions.

[Yongxi Lin (Aaron)]

I created a PR #31235 for this. The rest of the proof still works by using upgradeIsCompletelyMetrizable. This should be easy to review.

[Snir Broshi]

Nice! Didn't expect the proof could be fixed with only a single line change

[Snir Broshi]

This might also be an opportunity to rename the instance to BaireSpace.of_isCompletelyMetrizableSpace or similar, and deprecate the old name

[Etienne Marion]

This won't work because the instance you replaced did not assume T0Space so the hypothesis was actually completely pseudometrizable. Your change breaks docs#banach_steinhaus which only assumes SeminormedAddCommGroup.

[Moritz Doll]

I am not entire sure whethre assuming IsCompletelyMetrizableSpace is better than the complete uniform space with countable uniformity. The later is not common, but it feels more natural since uniform spaces are exactly the spaces where you can talk about completeness and having a filter being countably generated is reasonable condition. My impression in the theory of topological vector spaces is that people don't want to talk about uniform spaces (or don't know what they are), so they define Fréchet spaces as locally convex spaces that are metrizable and complete, but that metric is non-canonical and doesn't really serve a purpose.

[Aaron Liu]

well one implies the other and we generally want to be general

[Aaron Liu]

isn't IsCompletelyMetrizableSpace for exactly when we have a topology but no canonical metric?

[Moritz Doll]

Yeah, but you have to construct a metric. docs#UniformSpace.metricSpace gives you one, but than you have to prove IsCompletelyMetrizableSpace for the same assumptions without anything being gained and as @Etienne Marion said there is the T0Space instance as well, so if I understand everything correctly, then the PR makes the theorem worse (both in usability and strength).

[Aaron Liu]

sounds like we need completely pseudometrizable spaces

[Aaron Liu]

Moritz Doll said:

but than you have to prove IsCompletelyMetrizableSpace for the same assumptions without anything being gained

I am confused. What do you mean by this?

[Moritz Doll]

If I take my favorite space satisfies the current conditions, then I have to add an extra instance that basically just picks the metric I linked above to prove the IsCompletelyMetrizableSpace property to be able to use the Baire theorem.

[Moritz Doll]

But my real question here is: what is being gained from the proposed change?

[Aaron Liu]

Moritz Doll said:

If I take my favorite space satisfies the current conditions, then I have to add an extra instance that basically just picks the metric I linked above to prove the IsCompletelyMetrizableSpace property to be able to use the Baire theorem.

no it's an instance, right?

[Aaron Liu]

an instance that T0 complete uniform spaces with a countably generated uniformity are completely metrizable

[Moritz Doll]

yes, but you have to do that in every case where there is no canonical metric

[Moritz Doll]

docs#UniformSpace.metricSpace is not an instance (for a very good reason)

[Aaron Liu]

but we can have instances for metrizable spaces that aren't metric space instances

[Aaron Liu]

docs#TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable this is an instance

[Aaron Liu]

so if you have a complete T0 uniform space already you won't have to add an extra instance

[Aaron Liu]

like, this isn't any worse than right now, since right now, if I take my favorite space satisfying all the conditions, then I have to add an instance that it's a uniform space and that the uniform space is complete and has countably generated uniformity

[Moritz Doll]

Ok, so the reason I see is if you have a metrizable space where don't have any way of proving completeness using the uniformity directly would be more annoying currently.

[Yongxi Lin (Aaron)]

I believe originally the authors of Mathlib/Topology/Baire/CompleteMetrizable.lean proved that a completely PseudoEmetrizable space has the Baire property (although they assume that the space is uniform with a countable basis, but the proof really relies on completeness and PseudoEmetrizability). But do we really need a notion of completely PseudoEmetrizable (a space is completely PseudoEmetrizable iff there exists a PseudoEmetric space structure compatible with the topology which makes the space complete)? At least I have never seen this notion in other places of math.

[Yongxi Lin (Aaron)]

As shown below, the proof still works if I assume that X is a complete PseudoEMetricSpace. As [UniformSpace X] and [(uniformity X).IsCountablyGenerated] implies that X is pseudometrizable (UniformSpace.pseudoMetrizableSpace) and thus pseudoEMetrizable, I believe we should assume [IsCompletelyPseudoEMetrizable X] for the most general version of the first Baire theorem.

import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Topology.Metrizable.CompletelyMetrizable

open EMetric Set TopologicalSpace
open scoped ENNReal

variable {X : Type*} [PseudoEMetricSpace X] [CompleteSpace X]

instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace : BaireSpace X := by
  refine ⟨fun f ho hd => ?_⟩
  let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
  have Bpos : ∀ n, 0 < B n := fun n ↦
    ENNReal.div_pos one_ne_zero <| by finiteness
  have : ∀ n x δ, δ ≠ 0 → ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n := by
    intro n x δ δpos
    have : x ∈ closure (f n) := hd n x
    rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
    rw [edist_comm] at xy
    obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedBall y r ⊆ f n :=
      nhds_basis_closed_eball.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
    refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
    · show 0 < min (min (δ / 2) r) (B (n + 1))
      exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))
    · show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
      exact min_le_right _ _
    · show z ∈ closedBall x δ
      calc
        edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
        _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := add_le_add hz (le_of_lt xy)
        _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
        _ = δ := ENNReal.add_halves δ
    show z ∈ f n
    exact hr (calc
      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))
  choose! center radius Hpos HB Hball using this
  refine fun x => (mem_closure_iff_nhds_basis nhds_basis_closed_eball).2 fun ε εpos => ?_
  let F : ℕ → X × ℝ≥0∞ := fun n =>
    Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
  let c : ℕ → X := fun n => (F n).1
  let r : ℕ → ℝ≥0∞ := fun n => (F n).2
  have rpos : ∀ n, 0 < r n := by
    intro n
    induction n with
    | zero => exact lt_min εpos (Bpos 0)
    | succ n hn => exact Hpos n (c n) (r n) hn.ne'
  have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
  have rB : ∀ n, r n ≤ B n := by
    intro n
    cases n with
    | zero => exact min_le_right _ _
    | succ n => exact HB n (c n) (r n) (r0 n)
  have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n :=
    fun n => Hball n (c n) (r n) (r0 n)
  have cdist : ∀ n, edist (c n) (c (n + 1)) ≤ B n := by
    intro n
    rw [edist_comm]
    have A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1)) := mem_closedBall_self
    have I :=
      calc
        closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) :=
          Subset.trans (incl n) inter_subset_left
        _ ⊆ closedBall (c n) (B n) := closedBall_subset_closedBall (rB n)
    exact I A
  have : CauchySeq c := cauchySeq_of_edist_le_geometric_two _ ENNReal.one_ne_top cdist
  rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
  use y
  simp only [Set.mem_iInter]
  have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by
    intro n
    refine Nat.le_induction ?_ fun m _ h => ?_
    · exact Subset.refl _
    · exact Subset.trans (incl m) (Subset.trans inter_subset_left h)
  have yball : ∀ n, y ∈ closedBall (c n) (r n) := by
    intro n
    refine isClosed_closedBall.mem_of_tendsto ylim ?_
    refine (Filter.eventually_ge_atTop n).mono fun m hm => ?_
    exact I n m hm mem_closedBall_self
  constructor
  · show ∀ n, y ∈ f n
    intro n
    have : closedBall (c (n + 1)) (r (n + 1)) ⊆ f n :=
      Subset.trans (incl n) inter_subset_right
    exact this (yball (n + 1))
  change edist y x ≤ ε
  exact le_trans (yball 0) (min_le_left _ _)

[Aaron Liu]

pseudometrizable and pseudoEmetrizable are the same thing though?

[Aaron Liu]

since if you have an extended distance function edist then the distance fun x y => min 1 (edist x y) defines the same topology and is entirely real-valued

[Yongxi Lin (Aaron)]

I guess you mean min?

[Aaron Liu]

oh yeah

[Aaron Liu]

definitely min

[Yongxi Lin (Aaron)]

Aaron Liu said:

pseudometrizable and pseudoEmetrizable are the same thing though?

I think you are correct. Also I believe edist and fun x y => min 1 (edist x y) give rises to the same uniformity so that edist is complete iff fun x y => min 1 (edist x y) is complete (that is, a space is completely pseudoMetrizable iff it is completely pseudoEMetrizable).

[Yongxi Lin (Aaron)]

But again is there really an interest for an API about [IsCompletelyPseudoMetrizable]? I can go ahead and make a PR if the answer is Yes, but if not, I will only change the current docstring in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Baire/CompleteMetrizable.html#BaireSpace.of_pseudoEMetricSpace_completeSpace in #31235