English
An almost everywhere sequential limit of almost everywhere strongly measurable functions is almost everywhere strongly measurable.
Русский
Предел по почти всей последовательности функций, сходящихся почти всюду, является AEStronglyMeasurable.
LaTeX
$$$(\forall i, AEStronglyMeasurable(f_i, \mu)) \land (\forall^{ae} x, Tendsto(\lambda n. f_n x) u (\mathcal{N}(g x))) \Rightarrow AEStronglyMeasurable(g, \mu)$$$
Lean4
/-- An almost everywhere sequential limit of almost everywhere strongly measurable functions is
almost everywhere strongly measurable. -/
theorem _root_.aestronglyMeasurable_of_tendsto_ae {ι : Type*} [PseudoMetrizableSpace β] (u : Filter ι) [NeBot u]
[IsCountablyGenerated u] {f : ι → α → β} {g : α → β} (hf : ∀ i, AEStronglyMeasurable (f i) μ)
(lim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))) : AEStronglyMeasurable g μ :=
by
borelize β
refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩
· exact aemeasurable_of_tendsto_metrizable_ae _ (fun n => (hf n).aemeasurable) lim
· rcases u.exists_seq_tendsto with ⟨v, hv⟩
have : ∀ n : ℕ, ∃ t : Set β, IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ := fun n =>
(aestronglyMeasurable_iff_aemeasurable_separable.1 (hf (v n))).2
choose t t_sep ht using this
refine ⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩
filter_upwards [ae_all_iff.2 ht, lim] with x hx h'x
apply mem_closure_of_tendsto (h'x.comp hv)
filter_upwards with n using mem_iUnion_of_mem n (hx n)
