feat(measure_theory/constructions/borel_space): the set of points for…

… which a measurable sequence of functions converges is measurable (#15307)




Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

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,31 @@ 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
+  [hγ : opens_measurable_space γ] [countable ι] {l : filter ι}
+  [l.is_countably_generated] {f : ι → β → γ} (hf : ∀ i, measurable (f i)) :
+  measurable_set {x | ∃ c, tendsto (λ n, f n x) l (𝓝 c)} :=
+begin
+  by_cases hl : l.ne_bot,
+  swap, { rw not_ne_bot at hl, simp [hl] },
+  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 set.countable_univ (λ K _, _),
+  simp_rw set.set_of_exists,
+  refine measurable_set.bUnion set.countable_univ (λ N hN, _),
+  simp_rw [prod_image_image_eq, image_subset_iff, prod_subset_iff, set.set_of_forall],
+  exact measurable_set.bInter (to_countable (u N)) (λ i _,
+    measurable_set.bInter (to_countable (u N)) (λ j _,
+    measurable_set_lt (measurable.dist (hf i) (hf j)) measurable_const)),
+end
+
 end measure_theory

src/order/filter/bases.lean

@@ -707,6 +707,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