[Merged by Bors] - feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable

src/measure_theory/constructions/polish.lean

@@ -46,7 +46,7 @@ analytic sets.
 -/
 
 open set function polish_space pi_nat topological_space metric filter
-open_locale topological_space measure_theory
+open_locale topological_space measure_theory filter
 
 variables {α : Type*} [topological_space α] {ι : Type*}
 
@@ -580,10 +580,11 @@ begin
   { rwa inj_on_iff_injective at f_inj }
 end
 
-variables [measurable_space γ] [borel_space γ]
+
+variables [measurable_space γ] [hγb : borel_space γ]
 {β : Type*} [tβ : topological_space β] [t2_space β] [measurable_space β] [borel_space β]
 {s : set γ} {f : γ → β}
-include tβ
+include tβ hγb
 
 /-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a Polish space, then its image under
 a continuous injective map is also Borel-measurable. -/
@@ -680,4 +681,29 @@ begin
   simp only [id.def, image_id'],
 end
 
+omit hγb
+
+/-- The set of points for which a measurable sequence of functions converges is measurable. -/
+@[measurability] lemma measurable_set_exists_tendsto_at_top
+  [hγ : opens_measurable_space γ] [encodable ι] {l : filter ι} [hl : l.ne_bot]
+  [l.is_countably_generated] {f : ι → β → γ} (hf : ∀ i, measurable (f i)) :
+  measurable_set {x | ∃ c, tendsto (λ n, f n x) l (𝓝 c)} :=
+begin
+  letI := upgrade_polish_space γ,
+  rcases l.exists_antitone_basis with ⟨u, hu⟩,
+  simp_rw ← cauchy_map_iff_exists_tendsto,
+  change measurable_set {x | _ ∧ _},
+  have : ∀ x, ((map (λ i, f i x) l) ×ᶠ (map (λ i, f i x) l)).has_antitone_basis
+    (λ n, ((λ i, f i x) '' u n) ×ˢ ((λ i, f i x) '' u n)) := λ x, hu.map.prod hu.map,
+  simp_rw [and_iff_right (hl.map _), filter.has_basis.le_basis_iff (this _).to_has_basis
+    metric.uniformity_basis_dist_inv_nat_succ, set.set_of_forall],
+  refine measurable_set.bInter (countable_encodable _) (λ K _, _),
+  simp_rw set.set_of_exists,
+  refine measurable_set.bUnion (countable_encodable _) (λ N hN, _),
+  simp_rw [prod_image_image_eq, image_subset_iff, prod_subset_iff, set.set_of_forall],
+  exact measurable_set.bInter (countable_encodable _) (λ i _,
+    measurable_set.bInter (countable_encodable _) (λ j _,
+    measurable_set_lt (measurable.dist (hf i) (hf j)) measurable_const))
+end
+
 end measure_theory

src/order/filter/bases.lean

@@ -704,6 +704,11 @@ includes `s i` for some `i`, and `s` is decreasing. -/
   extends has_basis l (λ _, true) s : Prop :=
 (antitone : antitone s)
 
+lemma has_antitone_basis.map {l : filter α} {s : ι'' → set α} {m : α → β}
+  (hf : has_antitone_basis l s) :
+  has_antitone_basis (map m l) (λ n, m '' s n) :=
+⟨has_basis.map _ hf.to_has_basis, λ i j hij, image_subset _ $ hf.2 hij⟩
+
 end same_type
 
 section two_types