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