feat(topology/metric_space/baire): define filter residual (#3149)

Fixes #2265. Also define a typeclass `countable_Inter_filter` and prove that both `residual`
and `μ.ae` have this property.

Author: urkud

src/analysis/normed_space/banach.lean

@@ -43,8 +43,9 @@ begin
     refine mem_Union.2 ⟨n, subset_closure _⟩,
     refine (mem_image _ _ _).2 ⟨x, ⟨_, hx⟩⟩,
     rwa [mem_ball, dist_eq_norm, sub_zero] },
-  have : ∃(n:ℕ) y ε, 0 < ε ∧ ball y ε ⊆ closure (f '' (ball 0 n)) :=
+  have : ∃ (n : ℕ) x, x ∈ interior (closure (f '' (ball 0 n))) :=
     nonempty_interior_of_Union_of_closed (λn, is_closed_closure) A,
+  simp only [mem_interior_iff_mem_nhds, mem_nhds_iff] at this,
   rcases this with ⟨n, a, ε, ⟨εpos, H⟩⟩,
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
   refine ⟨(ε/2)⁻¹ * ∥c∥ * 2 * n, _, λy, _⟩,

src/measure_theory/measure_space.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import measure_theory.outer_measure
+import order.filter.countable_Inter
+
 /-!
 # Measure spaces
 
@@ -748,15 +750,21 @@ by simp only [ae_iff, not_not, set_of_mem_eq]
 lemma ae_of_all {p : α → Prop} (μ : measure α) : (∀a, p a) → ∀ₘ a ∂ μ, p a :=
 eventually_of_forall _
 
+instance : countable_Inter_filter μ.ae :=
+⟨begin
+  intros S hSc hS,
+  simp only [mem_ae_iff, compl_sInter, sUnion_image, bUnion_eq_Union] at hS ⊢,
+  haveI := hSc.to_encodable,
+  exact measure_Union_null (subtype.forall.2 hS)
+end⟩
+
 lemma ae_all_iff {ι : Type*} [encodable ι] {p : α → ι → Prop} :
   (∀ₘ a ∂ μ, ∀i, p a i) ↔ (∀i, ∀ₘ a ∂ μ, p a i) :=
-begin
-  refine iff.intro (assume h i, _) (assume h, _),
-  { filter_upwards [h] assume a ha, ha i },
-  { have h := measure_Union_null h,
-    rw [← compl_Inter] at h,
-    filter_upwards [h] assume a, mem_Inter.1 }
-end
+eventually_countable_forall
+
+lemma ae_ball_iff {ι} {S : set ι} (hS : countable S) {p : Π (x : α) (i ∈ S), Prop} :
+  (∀ₘ x ∂ μ, ∀ i ∈ S, p x i ‹_›) ↔ ∀ i ∈ S, ∀ₘ x ∂ μ, p x i ‹_› :=
+eventually_countable_ball hS
 
 lemma ae_eq_refl (f : α → β) : ∀ₘ a ∂ μ, f a = f a :=
 ae_of_all μ $ λ a, rfl

src/order/filter/countable_Inter.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import order.filter.basic
+import data.set.countable
+
+/-!
+# Filters with countable intersection property
+
+In this file we define `countable_Inter_filter` to be the class of filters with the following
+property: for any countable collection of sets `s ∈ l` their intersection belongs to `l` as well.
+
+Two main examples are the `residual` filter defined in `topology.metric_space.baire` and
+the `measure.ae` filter defined in `measure_theory.measure_space`.
+-/
+
+open set filter
+
+variables {ι α : Type*}
+
+/-- A filter `l` has the countable intersection property if for any countable collection
+of sets `s ∈ l` their intersection belongs to `l` as well. -/
+class countable_Inter_filter (l : filter α) : Prop :=
+(countable_sInter_mem_sets' :
+  ∀ {S : set (set α)} (hSc : countable S) (hS : ∀ s ∈ S, s ∈ l), ⋂₀ S ∈ l)
+
+variables {l : filter α} [countable_Inter_filter l]
+
+lemma countable_sInter_mem_sets {S : set (set α)} (hSc : countable S) :
+  ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l :=
+⟨λ hS s hs, mem_sets_of_superset hS (sInter_subset_of_mem hs),
+  countable_Inter_filter.countable_sInter_mem_sets' hSc⟩
+
+lemma countable_Inter_mem_sets [encodable ι] {s : ι → set α} :
+  (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l :=
+sInter_range s ▸ (countable_sInter_mem_sets (countable_range _)).trans forall_range_iff
+
+lemma countable_bInter_mem_sets {S : set ι} (hS : countable S) {s : Π i ∈ S, set α} :
+  (⋂ i ∈ S, s i ‹_›) ∈ l ↔  ∀ i ∈ S, s i ‹_› ∈ l :=
+begin
+  rw [bInter_eq_Inter],
+  haveI := hS.to_encodable,
+  exact countable_Inter_mem_sets.trans subtype.forall
+end
+
+lemma eventually_countable_forall [encodable ι] {p : α → ι → Prop} :
+  (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i :=
+by simpa only [filter.eventually, set_of_forall]
+  using @countable_Inter_mem_sets _ _ l _ _ (λ i, {x | p x i})
+
+lemma eventually_countable_ball {S : set ι} (hS : countable S) {p : Π (x : α) (i ∈ S), Prop} :
+  (∀ᶠ x in l, ∀ i ∈ S, p x i ‹_›) ↔ ∀ i ∈ S, ∀ᶠ x in l, p x i ‹_› :=
+by simpa only [filter.eventually, set_of_forall]
+  using @countable_bInter_mem_sets _ _ l _ _ hS (λ i hi, {x | p x i hi})
+
+instance countable_Inter_filter_principal (s : set α) : countable_Inter_filter (principal s) :=
+⟨λ S hSc hS, subset_sInter hS⟩
+
+instance countable_Inter_filter_bot : countable_Inter_filter (⊥ : filter α) :=
+by { rw ← principal_empty, apply countable_Inter_filter_principal }
+
+instance countable_Inter_filter_top : countable_Inter_filter (⊤ : filter α) :=
+by { rw ← principal_univ, apply countable_Inter_filter_principal }

src/topology/basic.lean

@@ -554,6 +554,17 @@ have 𝓝 a ⊓ principal (s ∩ t) ≠ ⊥,
     ... ≠ ⊥ : by rw [closure_eq_nhds] at ht; assumption,
 by rwa [closure_eq_nhds]
 
+lemma dense_inter_of_open_left {s t : set α} (hs : closure s = univ) (ht : closure t = univ)
+  (hso : is_open s) :
+  closure (s ∩ t) = univ :=
+eq_univ_of_subset (closure_minimal (closure_inter_open hso) is_closed_closure) $
+  by simp only [*, inter_univ]
+
+lemma dense_inter_of_open_right {s t : set α} (hs : closure s = univ) (ht : closure t = univ)
+  (hto : is_open t) :
+  closure (s ∩ t) = univ :=
+inter_comm t s ▸ dense_inter_of_open_left ht hs hto
+
 lemma closure_diff {s t : set α} : closure s - closure t ⊆ closure (s - t) :=
 calc closure s \ closure t = (- closure t) ∩ closure s : by simp only [diff_eq, inter_comm]
   ... ⊆ closure (- closure t ∩ s) : closure_inter_open $ is_open_compl_iff.mpr $ is_closed_closure

src/topology/instances/ennreal.lean

@@ -768,7 +768,7 @@ end
 
 theorem continuous_edist : continuous (λp:α×α, edist p.1 p.2) :=
 begin
-  apply continuous_of_le_add_edist 2 (by simp),
+  apply continuous_of_le_add_edist 2 (by norm_num),
   rintros ⟨x, y⟩ ⟨x', y'⟩,
   calc edist x y ≤ edist x x' + edist x' y' + edist y' y : edist_triangle4 _ _ _ _
     ... = edist x' y' + (edist x x' + edist y y') : by simp [edist_comm]; cc
@@ -795,6 +795,9 @@ begin
   exact cauchy_seq_of_edist_le_of_summable d hf hd
 end
 
+lemma emetric.is_closed_ball {a : α} {r : ennreal} : is_closed (closed_ball a r) :=
+is_closed_le (continuous_id.edist continuous_const) continuous_const
+
 /-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ennreal`,
 then the distance from `f n` to the limit is bounded by `∑'_{k=n}^∞ d k`. -/
 lemma edist_le_tsum_of_edist_le_of_tendsto {f : ℕ → α} (d : ℕ → ennreal)

src/topology/metric_space/baire.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.specific_limits
+import order.filter.countable_Inter
 
 /-!
 # Baire theorem
@@ -18,10 +19,13 @@ covered by a countable union of closed sets, then the union of their interiors i
 
 The names of the theorems do not contain the string "Baire", but are instead built from the form of
 the statement. "Baire" is however in the docstring of all the theorems, to facilitate grep searches.
+
+We also define the filter `residual α` generated by dense `Gδ` sets and prove that this filter
+has the countable intersection property.
 -/
 
 noncomputable theory
-open_locale classical
+open_locale classical topological_space
 
 open filter encodable set
 
@@ -86,18 +90,30 @@ end
 
 end is_Gδ
 
+/-- A set `s` is called *residual* if it includes a dense `Gδ` set. If `α` is a Baire space
+(e.g., a complete metric space), then residual sets form a filter, see `mem_residual`.
+
+ For technical reasons we define the filter `residual` in any topological space
+ but in a non-Baire space it is not useful because it may contain some non-residual
+ sets. -/
+def residual (α : Type*) [topological_space α] : filter α :=
+⨅ t (ht : is_Gδ t) (ht' : closure t = univ), principal t
+
 section Baire_theorem
-open metric
-variables [metric_space α] [complete_space α]
+open emetric ennreal
+variables [emetric_space α] [complete_space α]
 
 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here when
 the source space is ℕ (and subsumed below by `dense_Inter_of_open` working with any
 encodable source space). -/
 theorem dense_Inter_of_open_nat {f : ℕ → set α} (ho : ∀n, is_open (f n))
   (hd : ∀n, closure (f n) = univ) : closure (⋂n, f n) = univ :=
 begin
-  let B : ℕ → ℝ := λn, ((1/2)^n : ℝ),
-  have Bpos : ∀n, 0 < B n := λn, begin apply pow_pos, by norm_num end,
+  let B : ℕ → ennreal := λn, 1/2^n,
+  have Bpos : ∀n, 0 < B n,
+  { intro n,
+    simp only [B, div_def, one_mul, ennreal.inv_pos],
+    exact pow_ne_top two_ne_top },
   /- Translate the density assumption into two functions `center` and `radius` associating
   to any n, x, δ, δpos a center and a positive radius such that
   `closed_ball center radius` is included both in `f n` and in `closed_ball x δ`.
@@ -106,40 +122,40 @@ begin
   { assume n x δ,
     by_cases δpos : δ > 0,
     { have : x ∈ closure (f n) := by simpa only [(hd n).symm] using mem_univ x,
-      rcases metric.mem_closure_iff.1 this (δ/2) (half_pos δpos) with ⟨y, ys, xy⟩,
-      rw dist_comm at xy,
-      rcases is_open_iff.1 (ho n) y ys with ⟨r, rpos, hr⟩,
-      refine ⟨y, min (min (δ/2) (r/2)) (B (n+1)), λ_, ⟨_, _, λz hz, ⟨_, _⟩⟩⟩,
-      show 0 < min (min (δ / 2) (r/2)) (B (n+1)),
-        from lt_min (lt_min (half_pos δpos) (half_pos rpos)) (Bpos (n+1)),
-      show min (min (δ / 2) (r/2)) (B (n+1)) ≤ B (n+1), from min_le_right _ _,
+      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, closed_ball y r ⊆ f n :=
+        nhds_basis_closed_eball.mem_iff.1 (is_open_iff_mem_nhds.1 (ho n) y ys),
+      refine ⟨y, min (min (δ/2) r) (B (n+1)), λ_, ⟨_, _, λz hz, ⟨_, _⟩⟩⟩,
+      show 0 < min (min (δ / 2) r) (B (n+1)),
+        from lt_min (lt_min (ennreal.half_pos δpos) rpos) (Bpos (n+1)),
+      show min (min (δ / 2) r) (B (n+1)) ≤ B (n+1), from min_le_right _ _,
       show z ∈ closed_ball x δ, from calc
-        dist z x ≤ dist z y + dist y x : dist_triangle _ _ _
-        ... ≤ (min (min (δ / 2) (r/2)) (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_refl _)
-        ... = δ : add_halves _,
+        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_refl _)
+        ... = δ : ennreal.add_halves δ,
       show z ∈ f n, from hr (calc
-        dist z y ≤ min (min (δ / 2) (r/2)) (B (n+1)) : hz
-        ... ≤ r/2 : le_trans (min_le_left _ _) (min_le_right _ _)
-        ... < r : half_lt_self rpos) },
+        edist z y ≤ min (min (δ / 2) r) (B (n+1)) : hz
+        ... ≤ r : le_trans (min_le_left _ _) (min_le_right _ _)) },
     { use [x, 0] }},
   choose center radius H using this,
 
   refine subset.antisymm (subset_univ _) (λx hx, _),
-  refine metric.mem_closure_iff.2 (λε εpos, _),
+  refine (mem_closure_iff_nhds_basis nhds_basis_closed_eball).2 (λ ε εpos, _),
   /- ε is positive. We have to find a point in the ball of radius ε around x belonging to all `f n`.
   For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball
   `closed_ball (c n) (r n)` is included in the previous ball and in `f n`, and such that
   `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a
   limit which belongs to all the `f n`. -/
-  let F : ℕ → (α × ℝ) := λn, nat.rec_on n (prod.mk x (min (ε/2) 1))
+  let F : ℕ → (α × ennreal) := λn, nat.rec_on n (prod.mk x (min ε (B 0)))
                               (λn p, prod.mk (center n p.1 p.2) (radius n p.1 p.2)),
   let c : ℕ → α := λn, (F n).1,
-  let r : ℕ → ℝ := λn, (F n).2,
+  let r : ℕ → ennreal := λn, (F n).2,
   have rpos : ∀n, r n > 0,
   { assume n,
     induction n with n hn,
-    exact lt_min (half_pos εpos) (zero_lt_one),
+    exact lt_min εpos (Bpos 0),
     exact (H n (c n) (r n) hn).1 },
   have rB : ∀n, r n ≤ B n,
   { assume n,
@@ -148,20 +164,17 @@ begin
     exact (H n (c n) (r n) (rpos n)).2.1 },
   have incl : ∀n, closed_ball (c (n+1)) (r (n+1)) ⊆ (closed_ball (c n) (r n)) ∩ (f n) :=
     λn, (H n (c n) (r n) (rpos n)).2.2,
-  have cdist : ∀n, dist (c n) (c (n+1)) ≤ B n,
+  have cdist : ∀n, edist (c n) (c (n+1)) ≤ B n,
   { assume n,
-    rw dist_comm,
-    have A : c (n+1) ∈ closed_ball (c (n+1)) (r (n+1)) :=
-      mem_closed_ball_self (le_of_lt (rpos (n+1))),
+    rw edist_comm,
+    have A : c (n+1) ∈ closed_ball (c (n+1)) (r (n+1)) := mem_closed_ball_self,
     have I := calc
       closed_ball (c (n+1)) (r (n+1)) ⊆ closed_ball (c n) (r n) :
         subset.trans (incl n) (inter_subset_left _ _)
       ... ⊆ closed_ball (c n) (B n) : closed_ball_subset_closed_ball (rB n),
     exact I A },
-  have : cauchy_seq c,
-  { refine cauchy_seq_of_le_geometric (1/2) 1 (by norm_num) (λn, _),
-    rw one_mul,
-    exact cdist n },
+  have : cauchy_seq c :=
+    cauchy_seq_of_edist_le_geometric_two _ one_ne_top cdist,
   -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
   rcases cauchy_seq_tendsto_of_complete this with ⟨y, ylim⟩,
   -- this point `y` will be the desired point. We will check that it belongs to all
@@ -177,16 +190,13 @@ begin
   { assume n,
     refine mem_of_closed_of_tendsto (by simp) ylim is_closed_ball _,
     simp only [filter.mem_at_top_sets, nonempty_of_inhabited, set.mem_preimage],
-    exact ⟨n, λm hm, I n m hm (mem_closed_ball_self (le_of_lt (rpos m)))⟩ },
+    exact ⟨n, λm hm, I n m hm mem_closed_ball_self⟩ },
   split,
   show ∀n, y ∈ f n,
   { assume n,
     have : closed_ball (c (n+1)) (r (n+1)) ⊆ f n := subset.trans (incl n) (inter_subset_right _ _),
     exact this (yball (n+1)) },
-  show dist x y < ε, from calc
-    dist x y = dist y x : dist_comm _ _
-    ... ≤ r 0 : yball 0
-    ... < ε : lt_of_le_of_lt (min_le_left _ _) (half_lt_self εpos)
+  show edist y x ≤ ε, from le_trans (yball 0) (min_le_left _ _),
 end
 
 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀. -/
@@ -272,6 +282,35 @@ begin
   apply dense_Inter_of_Gδ; simp [bool.forall_bool, *]
 end
 
+/-- A property holds on a residual (comeagre) set if and only if it holds on some dense `Gδ` set. -/
+lemma eventually_residual {p : α → Prop} :
+  (∀ᶠ x in residual α, p x) ↔ ∃ (t : set α), is_Gδ t ∧ closure t = univ ∧ ∀ x ∈ t, p x :=
+calc (∀ᶠ x in residual α, p x) ↔
+  ∀ᶠ x in ⨅ (t : set α) (ht : is_Gδ t ∧ closure t = univ), principal t, p x :
+    by simp only [residual, infi_and]
+... ↔ ∃ (t : set α) (ht : is_Gδ t ∧ closure t = univ), ∀ᶠ x in principal t, p x :
+  mem_binfi (λ t₁ h₁ t₂ h₂, ⟨t₁ ∩ t₂, ⟨h₁.1.inter h₂.1, dense_inter_of_Gδ h₁.1 h₂.1 h₁.2 h₂.2⟩,
+    by simp⟩) ⟨univ, is_Gδ_univ, closure_univ⟩
+... ↔ _ : by simp [and_assoc]
+
+/-- A set is residual (comeagre) if and only if it includes a dense `Gδ` set. -/
+lemma mem_residual {s : set α} :
+  s ∈ residual α ↔ ∃ t ⊆ s, is_Gδ t ∧ closure t = univ :=
+(@eventually_residual α _ _ (λ x, x ∈ s)).trans $ exists_congr $
+λ t, by rw [exists_prop, and_comm (t ⊆ s), subset_def, and_assoc]
+
+instance : countable_Inter_filter (residual α) :=
+⟨begin
+  intros S hSc hS,
+  simp only [mem_residual] at *,
+  choose T hTs hT using hS,
+  refine ⟨⋂ s ∈ S, T s ‹_›, _, _, _⟩,
+  { rw [sInter_eq_bInter],
+    exact Inter_subset_Inter (λ s, Inter_subset_Inter $ hTs s) },
+  { exact is_Gδ_bInter hSc (λ s hs, (hT s hs).1) },
+  { exact dense_bInter_of_Gδ (λ s hs, (hT s hs).1) hSc (λ s hs, (hT s hs).2) }
+end⟩
+
 /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
 are dense. Formulated here with an index set which is a countable set in any type. -/
 theorem dense_bUnion_interior_of_closed {S : set β} {f : β → set α} (hc : ∀s∈S, is_closed (f s))
@@ -319,18 +358,14 @@ end
 /-- One of the most useful consequences of Baire theorem: if a countable union of closed sets
 covers the space, then one of the sets has nonempty interior. -/
 theorem nonempty_interior_of_Union_of_closed [nonempty α] [encodable β] {f : β → set α}
-  (hc : ∀s, is_closed (f s)) (hU : (⋃s, f s) = univ) : ∃s x ε, 0 < ε ∧ ball x ε ⊆ f s :=
+  (hc : ∀s, is_closed (f s)) (hU : (⋃s, f s) = univ) :
+  ∃s, (interior $ f s).nonempty :=
 begin
-  have : ∃s, (interior (f s)).nonempty,
-  { by_contradiction h,
-    simp only [not_exists, not_nonempty_iff_eq_empty] at h,
-    have := calc ∅ = closure (⋃s, interior (f s)) : by simp [h]
-                 ... = univ : dense_Union_interior_of_closed hc hU,
-    exact univ_nonempty.ne_empty this.symm },
-  rcases this with ⟨s, hs⟩,
-  rcases hs with ⟨x, hx⟩,
-  rcases mem_nhds_iff.1 (mem_interior_iff_mem_nhds.1 hx) with ⟨ε, εpos, hε⟩,
-  exact ⟨s, x, ε, εpos, hε⟩,
+  by_contradiction h,
+  simp only [not_exists, not_nonempty_iff_eq_empty] at h,
+  have := calc ∅ = closure (⋃s, interior (f s)) : by simp [h]
+             ... = univ : dense_Union_interior_of_closed hc hU,
+  exact univ_nonempty.ne_empty this.symm
 end
 
 end Baire_theorem

src/topology/metric_space/basic.lean

@@ -553,7 +553,7 @@ theorem nhds_basis_ball_inv_nat_pos :
 nhds_basis_uniformity uniformity_basis_dist_inv_nat_pos
 
 theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s :=
-by simp only [is_open_iff_nhds, mem_nhds_iff, le_principal_iff]
+by simp only [is_open_iff_mem_nhds, mem_nhds_iff]
 
 theorem is_open_ball : is_open (ball x ε) :=
 is_open_iff.2 $ λ y, exists_ball_subset_ball

src/topology/metric_space/emetric_space.lean

@@ -566,6 +566,9 @@ by rw [emetric.ball_eq_empty_iff]
 theorem nhds_basis_eball : (𝓝 x).has_basis (λ ε:ennreal, 0 < ε) (ball x) :=
 nhds_basis_uniformity uniformity_basis_edist
 
+theorem nhds_basis_closed_eball : (𝓝 x).has_basis (λ ε:ennreal, 0 < ε) (closed_ball x) :=
+nhds_basis_uniformity uniformity_basis_edist_le
+
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem nhds_eq : 𝓝 x = (⨅ε>0, principal (ball x ε)) :=
 nhds_basis_eball.eq_binfi