measurable_of_tendsto_metrizable_ae

English

If g is uniformly approximated by AEMeasurable functions f with arbitrary accuracy, then g is AEMeasurable.

Русский

Если функция g аппроксимируется почти пожалуй A.E.-измеримыми функциями f с любой точностью, то g — A.E.-измерима.

LaTeX

$$$\\forall \\varepsilon>0, \\exists f: AEMeasurable(f, μ) \\land \\forall x, dist(f(x), g(x)) ≤ \\varepsilon$ implies AEMeasurable g μ$$

Lean4

theorem measurable_of_tendsto_metrizable_ae {μ : Measure α} [μ.IsComplete] {f : ℕ → α → β} {g : α → β}
    (hf : ∀ n, Measurable (f n)) (h_ae_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) : Measurable g :=
  aemeasurable_iff_measurable.mp (aemeasurable_of_tendsto_metrizable_ae' (fun i => (hf i).aemeasurable) h_ae_tendsto)

Похожие утверждения