## Stream: maths

### Topic: A proof of Baire category theorem using #2850

#### 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                   : 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