[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/borel_space.lean

@@ -1496,6 +1496,27 @@ begin
   exact h's.closure_eq.symm
 end
 
+/-- The set of points for which a measurable sequence of functions converges is measurable. -/
+@[measurability] lemma measurable_set_exists_tendsto_at_top {ι : Type*}
+  [second_countable_topology α] [complete_space α] [nonempty ι] [encodable ι] [semilattice_sup ι]
+  {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
+  measurable_set {x | ∃ c, tendsto (λ n, f n x) at_top (𝓝 c)} :=
+begin
+  simp_rw ← cauchy_map_iff_exists_tendsto,
+  change measurable_set {x | cauchy_seq (λ n, f n x)},
+  simp_rw metric.cauchy_seq_iff'',
+  rw set.set_of_forall,
+  refine measurable_set.Inter (λ K, _),
+  rw set.set_of_exists,
+  refine measurable_set.Union (λ N, _),
+  rw set.set_of_forall,
+  refine measurable_set.Inter (λ n, _),
+  by_cases hNn : N ≤ n,
+  { simp only [hNn, ge_iff_le, forall_true_left],
+    exact measurable_set_lt (measurable.dist (hf n) (hf N)) measurable_const },
+  { simp only [hNn, ge_iff_le, is_empty.forall_iff, set_of_true, measurable_set.univ], }
+end
+
 end pseudo_metric_space
 
 /-- Given a compact set in a proper space, the measure of its `r`-closed thickenings converges to

src/topology/metric_space/basic.lean

@@ -1310,6 +1310,22 @@ theorem metric.cauchy_seq_iff' {u : β → α} :
   cauchy_seq u ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) (u N) < ε :=
 uniformity_basis_dist.cauchy_seq_iff'
 
+/-- A variation of `metric.cauchy_seq_iff'` where we only check the Cauchy condition for
+countably many bounds.
+
+This is useful whenever we want to show measurability of a set related to Cauchy sequences. -/
+lemma metric.cauchy_seq_iff'' {u : β → α} :
+  cauchy_seq u ↔ ∀ K : ℕ, ∃ N, ∀ n ≥ N, dist (u n) (u N) < (K + 1)⁻¹ :=
+begin
+  rw metric.cauchy_seq_iff',
+  refine ⟨λ h K, h (K + 1)⁻¹ (inv_pos.2 K.cast_add_one_pos), λ h ε hε, _⟩,
+  obtain ⟨K, hK⟩ := exists_nat_gt ε⁻¹,
+  obtain ⟨N, hN⟩ := h K,
+  refine ⟨N, λ n hn, lt_of_lt_of_le (hN n hn) _⟩,
+  rw [inv_le (K.cast_add_one_pos : (0 : ℝ) < K + 1) hε, ← nat.cast_one, ← nat.cast_add],
+  exact hK.le.trans (nat.cast_le.2 K.le_succ),
+end
+
 /-- In a pseudometric space, unifom Cauchy sequences are characterized by the fact that, eventually,
 the distance between all its elements is uniformly, arbitrarily small -/
 @[nolint ge_or_gt] -- see Note [nolint_ge]