English
Let {f_n} be a sequence of almost everywhere strongly measurable functions f_n : α → β that converge almost everywhere to some limit value l(x) (i.e., for μ-a.e. x, there exists l with f_n(x) → l). Then there exists a function f_lim : α → β which is strongly measurable and, for μ-almost every x, f_n(x) → f_lim(x) as n → ∞.
Русский
Пусть последовательность почти везде сильно измеримых функций f_n : α → β сходится почти повсеместно к некоторому значению l(x). Существуют функция-ограничение f_lim : α → β и т.д.: f_lim существенно измерима и почти везде выполняется предел f_n(x) → f_lim(x).
LaTeX
$$$\exists f_{lim}: \alpha \to \beta,\; \text{StronglyMeasurable}(f_{lim}) \\wedge \\ \forall^* x \partial\mu, \ Tendsto (n \mapsto f_n(x))_{n \to \infty} (\mathcal{N} (f_{lim}(x))).$$$
Lean4
/-- If a sequence of almost everywhere strongly measurable functions converges almost everywhere,
one can select a strongly measurable function as the almost everywhere limit. -/
theorem _root_.exists_stronglyMeasurable_limit_of_tendsto_ae [PseudoMetrizableSpace β] {f : ℕ → α → β}
(hf : ∀ n, AEStronglyMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, Tendsto (fun n => f n x) atTop (𝓝 l)) :
∃ f_lim : α → β, StronglyMeasurable f_lim ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x)) :=
by
borelize β
obtain ⟨g, _, hg⟩ : ∃ g : α → β, Measurable g ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) :=
measurable_limit_of_tendsto_metrizable_ae (fun n => (hf n).aemeasurable) h_ae_tendsto
have Hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hg
refine ⟨Hg.mk g, Hg.stronglyMeasurable_mk, ?_⟩
filter_upwards [hg, Hg.ae_eq_mk] with x hx h'x
rwa [h'x] at hx
