Zulip Chat Archive

Stream: maths

Topic: A proof of Baire category theorem using #2850


view this post on Zulip David Wärn (May 31 2020 at 18:43):

In an attempt to better explain the point of PR #2850, here is a proof of BCT for a complete metric space X (of course there is already a shorter proof in mathlib). The idea is to consider the poset of closed subsets C of X with nonempty interior, ordered by reverse inclusion. We have two families of predicates on this poset: one saying "C has diameter <= r", and one saying "C is a subset of S". We separately show that these predicates are both "cofinal", in the sense that any C can be shrunk so as to satisfy the predicate, assuming r > 0 and S open dense, respectively. #2850 finishes the job, more or less.

import order.generic_cofilter
import analysis.specific_limits

/- This is an attempt at illustrating the use #2850.

-/

open metric set

variables {α : Type*} [metric_space α]

-- where can I find this lemma?
lemma closed_ball_subset_ball (x : α) {a b : } (h : a < b) :
  closed_ball x a  ball x b :=
λ y hy, calc dist y x  a : hy
                  ... < b : h

-- where can I find this lemma?
lemma metric_space_is_regular (x : α) (s : set α) (ho : is_open s) (xs : x  s) :
   t : set α, is_open t  x  t  closure t  s :=
begin
  rcases metric.is_open_iff.mp ho x xs with r, rpos, xrs,
  refine ball x (r/2), is_open_ball, mem_ball_self (half_pos rpos), _⟩,
  calc closure (ball x (r/2))  closed_ball x (r/2) : closure_ball_subset_closed_ball
                          ...  ball x r : closed_ball_subset_ball x (half_lt_self rpos)
                          ...  s : xrs
end

variable (α)
/-- The type of closed subsets of `α` with nonempty interior. -/
def cniset : Type _ :=
  { C : set α // is_closed C  (interior C).nonempty }
variable {α}

/-- We order cnisets by reverse inclusion. A smaller cniset is thought of as
    'extending' a larger set, because it imposes more constraints. -/
instance : preorder (cniset α) :=
{ le := λ f g, g.val  f.val,
  le_refl := by tidy, le_trans := by tidy, }

/-- Given a dense open set `s`, any cniset can be shrunk so as to lie in `s`. -/
def cofinal_of_dense (s : set α) (ho : is_open s) (hd : closure s = univ) :
  { D : set (cniset α) // cofinal D } :=
{ val := { f | f.val  s},
  property :=
    begin
      rintros C, hc, hni,
      rcases dense_iff_inter_open.mp hd (interior C) (is_open_interior) hni
        with x, xic, xs,
      rcases metric_space_is_regular x (s  interior C) (is_open_inter ho $ is_open_interior)
        xs, xic with t, hto, xt, ht,
      rw subset_inter_iff at ht,
      refine ⟨⟨closure t, is_closed_closure, _⟩, _, _⟩,
      { use x,
        rw mem_interior,
        exact t, subset_closure, hto, xt, },
      exact ht.1,
      calc closure t  interior C : ht.2
                 ...  C : interior_subset
    end }

/-- Given `r > 0`, any cniset can be shrunk so as to have diameter `≤ r`:
    simply pick a point in the interior and intersect with the `r/2`-ball around it. -/
def cofinal_of_radius (r : ) (rpos : r > 0) :
  { D : set (cniset α) // cofinal D } :=
{ val := { f |  (x y  f.val), dist x y  r },
  property :=
    begin
      rintro C, hc, nic,
      cases nic with x hx,
      refine ⟨⟨C  closed_ball x (r/2), is_closed_inter hc is_closed_ball, _⟩, _, _⟩,
      { rw interior_inter,
        refine x, hx, _⟩,
        rw mem_interior,
        exact ball x (r/2), ball_subset_closed_ball, is_open_ball,
          mem_ball_self $ half_pos rpos, },
      { rintros a b ⟨_, ha ⟨_, hb,
        calc dist a b  dist a x + dist b x : dist_triangle_right _ _ _
                  ...  r/2 + r/2           : add_le_add ha hb
                  ... = r                   : add_halves r },
      apply inter_subset_left,
    end }

variables {ι : Type*} [encodable ι] ( : ι  { s : set α // is_open s  closure s = univ })

noncomputable def cofinal_family : ι    { D : set (cniset α) // cofinal D }
| (sum.inl i) := cofinal_of_dense ( i).val ( i).property.1 ( i).property.2
| (sum.inr n) := cofinal_of_radius (1 / (n+1)) nat.one_div_pos_of_nat

variable (st : cniset α)

def gencof : set (cniset α) := generic.cofilter st $ cofinal_family 

def filt : filter α :=
{ sets := { x |  y  gencof  st, subtype.val y  x },
  univ_sets := st, generic.starting_point_mem st _, subset_univ _⟩,
  sets_of_superset := λ x x' y, hy, hyx hs, y, hy, subset.trans hyx hs,
  inter_sets :=
    begin
      rintros x x' y, hy, hyx y', hy', hyx',
      rcases generic.directed_on st (cofinal_family ) y hy y' hy' with z, hz, hzy, hzy',
      refine z, hz, _⟩,
      calc z.val  y.val  y'.val : subset_inter hzy hzy'
             ...  x      x'     : inter_subset_inter hyx hyx'
    end }

lemma filt.cauchy : cauchy (filt  st) :=
begin
  rw metric.cauchy_iff,
  split,
  { suffices : ¬   filt  st,
    { intro h,
      rw h at this,
      tauto, },
    rintros y, hy, h,
    cases y.property.2 with w hw,
    exact h (interior_subset hw), },
  intros ε epos,
  cases exists_nat_one_div_lt epos with n nh,
  rcases generic.meets st (cofinal_family ) (sum.inr n) with y, hy, hyn,
  refine y.val, y, hy, subset.refl _⟩, _⟩,
  intros a b ha hb,
  calc dist a b  1 / (n+1) : hyn a b ha hb
            ... < ε         : nh
end

variable [complete_space α]

theorem baire' : (st.val   i, ( i).val).nonempty :=
begin
  cases complete_space.complete (filt.cauchy  st) with x hx,
  refine x, _, _⟩,
  { apply mem_of_closed_of_tendsto (filt.cauchy  st).1 hx st.property.1,
    refine ⟨_, _, subset.refl _⟩,
    apply generic.starting_point_mem, },
  { rw mem_Inter,
    intro i,
    rcases generic.meets st (cofinal_family ) (sum.inl i)
      with C, C_cf, hc,
    apply hc,
    apply mem_of_closed_of_tendsto (filt.cauchy  st).1 hx C.property.1,
    exact ⟨_, C_cf, subset.refl _⟩, },
end

I am curious about what people think of this style of proof! Do we have something like this in mathlib already?


Last updated: May 14 2021 at 19:21 UTC