English
There exists a measurable limit f_lim such that f_n → f_lim a.e. along μ.
Русский
Существование измеримого предела f_lim such that f_n → f_lim почти всюду.
LaTeX
$$$\\exists f\_lim: \\alpha \\to \\beta, Measurable(f\_lim) \\land \\forall^* x, Tendsto (f\_n x) \\to f\_lim x$$$
Lean4
theorem aemeasurable_of_unif_approx {β} [MeasurableSpace β] [PseudoMetricSpace β] [BorelSpace β] {μ : Measure α}
{g : α → β} (hf : ∀ ε > (0 : ℝ), ∃ f : α → β, AEMeasurable f μ ∧ ∀ᵐ x ∂μ, dist (f x) (g x) ≤ ε) :
AEMeasurable g μ :=
by
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto (0 : ℝ)
choose f Hf using fun n : ℕ => hf (u n) (u_pos n)
have : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) :=
by
have : ∀ᵐ x ∂μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 fun n => (Hf n).2
filter_upwards [this]
intro x hx
rw [tendsto_iff_dist_tendsto_zero]
exact squeeze_zero (fun n => dist_nonneg) hx u_lim
exact aemeasurable_of_tendsto_metrizable_ae' (fun n => (Hf n).1) this
