English
The set of x such that there exists c with Tendsto (f_n x) to c is measurable.
Русский
Существует c, такой что Tendsto; множество измеримо.
LaTeX
$$MeasurableSet {x | ∃ c, Tendsto (f_n x) l (nhds c)}$$
Lean4
/-- The set of points for which a measurable sequence of functions converges is measurable. -/
@[measurability]
theorem measurableSet_exists_tendsto [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ]
[hγ : OpensMeasurableSpace γ] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → β → γ}
(hf : ∀ i, Measurable (f i)) : MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)} :=
by
rcases l.eq_or_neBot with rfl | hl
· simp
letI := TopologicalSpace.upgradeIsCompletelyMetrizable γ
rcases l.exists_antitone_basis with ⟨u, hu⟩
simp_rw [← cauchy_map_iff_exists_tendsto]
change MeasurableSet {x | _ ∧ _}
have : ∀ x, (map (f · x) l ×ˢ map (f · x) l).HasAntitoneBasis fun n => ((f · x) '' u n) ×ˢ ((f · x) '' u n) :=
fun x => (hu.map _).prod (hu.map _)
simp_rw [and_iff_right (hl.map _),
Filter.HasBasis.le_basis_iff (this _).toHasBasis Metric.uniformity_basis_dist_inv_nat_succ, Set.setOf_forall]
refine MeasurableSet.biInter Set.countable_univ fun K _ => ?_
simp_rw [Set.setOf_exists, true_and]
refine MeasurableSet.iUnion fun N => ?_
simp_rw [prod_image_image_eq, image_subset_iff, prod_subset_iff, Set.setOf_forall]
exact
MeasurableSet.biInter (to_countable (u N)) fun i _ =>
MeasurableSet.biInter (to_countable (u N)) fun j _ =>
measurableSet_lt (Measurable.dist (hf i) (hf j)) measurable_const
