aemeasurable — Mathlib

English

If f_n are AEMeasurable and TendstoInMeasure μ f u g, then g is AEMeasurable.

Русский

Если f_n а.е.-измеримы и TendstoInMeasure(μ, f, u, g), то g а.е.-измерима.

LaTeX

$$$(\forall n, AEMeasurable(f_n, μ)) \wedge TendstoInMeasure(μ, f, u, g) \Rightarrow AEMeasurable(g, μ)$$$

Lean4

theorem aemeasurable {u : Filter ι} [NeBot u] [IsCountablyGenerated u] {f : ι → α → E} {g : α → E}
    (hf : ∀ n, AEMeasurable (f n) μ) (h_tendsto : TendstoInMeasure μ f u g) : AEMeasurable g μ :=
  by
  obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'
  exact aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns

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