exists_seq_tendsto_ae' — Mathlib

English

Supersedes by constructing a sequence ns such that TendstoInMeasure holds for f∘ns and further subsequences yield ae convergence.

Русский

Замещает построение подпоследовательности так, чтобы выполнялось сходимость по мере для f ∘ ns и далее подпоследовательности даёт ae-сходимость.

LaTeX

$$$\exists ns: \mathbb{N}\to \mathbb{N},\; Tendsto ns\ atTop\ u\;\wedge\; \forall^{ae} x,\; Tendsto (\lambda i, f(ns(i))(x)) atTop (nhds (g(x))).$$$

Lean4

theorem exists_seq_tendsto_ae' {u : Filter ι} [NeBot u] [IsCountablyGenerated u] {f : ι → α → E} {g : α → E}
    (hfg : TendstoInMeasure μ f u g) :
    ∃ ns : ℕ → ι, Tendsto ns atTop u ∧ ∀ᵐ x ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) :=
  by
  obtain ⟨ms, hms1, hms2⟩ := hfg.exists_seq_tendstoInMeasure_atTop
  obtain ⟨ns, hns1, hns2⟩ := hms2.exists_seq_tendsto_ae
  exact ⟨ms ∘ ns, hms1.comp hns1.tendsto_atTop, hns2⟩

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