English
The limit of a sequence of strongly measurable functions (under suitable convergence) is strongly measurable.
Русский
Предел последовательности сильно измеримых функций сохраняет сильную измеримость.
LaTeX
$$$\forall i, \mathrm{StronglyMeasurable}(f_i) \land \lim_i f_i = g \Rightarrow \mathrm{StronglyMeasurable}(g)$$$
Lean4
/-- A sequential limit of strongly measurable functions is strongly measurable. -/
theorem _root_.stronglyMeasurable_of_tendsto {ι : Type*} {m : MeasurableSpace α} [TopologicalSpace β]
[PseudoMetrizableSpace β] (u : Filter ι) [NeBot u] [IsCountablyGenerated u] {f : ι → α → β} {g : α → β}
(hf : ∀ i, StronglyMeasurable (f i)) (lim : Tendsto f u (𝓝 g)) : StronglyMeasurable g :=
by
borelize β
refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
· exact measurable_of_tendsto_metrizable' u (fun i => (hf i).measurable) lim
· rcases u.exists_seq_tendsto with ⟨v, hv⟩
have : IsSeparable (closure (⋃ i, range (f (v i)))) := .closure <| .iUnion fun i => (hf (v i)).isSeparable_range
apply this.mono
rintro _ ⟨x, rfl⟩
rw [tendsto_pi_nhds] at lim
apply mem_closure_of_tendsto ((lim x).comp hv)
filter_upwards with n
apply mem_iUnion_of_mem n
exact mem_range_self _
