English
If f_n is a sequence of AEMeasurable functions and f_n converges a.e. to g along atTop, then g is AEMeasurable.
Русский
Если последовательность A.E.-измеримых функций сходится почти везде к g по atTop, то g — A.E.-измерима.
LaTeX
$$$AEMeasurable f_n \\mu \\Rightarrow AEMeasurable g \\mu$ under ae-tendsto$$
Lean4
theorem aemeasurable_of_tendsto_metrizable_ae {ι} {μ : Measure α} {f : ι → α → β} {g : α → β} (u : Filter ι)
[hu : NeBot u] [IsCountablyGenerated u] (hf : ∀ n, AEMeasurable (f n) μ)
(h_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) u (𝓝 (g x))) : AEMeasurable g μ := by
classical
rcases u.exists_seq_tendsto with ⟨v, hv⟩
have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by filter_upwards [h_tendsto] with x hx using hx.comp hv
set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
refine
⟨aeSeqLim, measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p) (tendsto_pi_nhds.mpr fun x => ?_), ?_⟩
· simp_rw [aeSeqLim, aeSeq]
split_ifs with hx
· simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
· exact tendsto_const_nhds
·
exact
(ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
(aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
