exists_seq_tendstoInMeasure_atTop

English

If f tends to g in measure along u, then there exists a subsequence ns such that TendstoInMeasure μ (f ∘ ns) atTop u g along to a.e.

Русский

Если f сходится по мере к g вдоль u, то существует подпоследовательность ns такая, что TendstoInMeasure μ (f ∘ ns) к g почти всюду.

LaTeX

$$$\exists ns: \mathbb{N}\to \mathbb{N},\; Tendsto(\text{ns})\;atTop\;u\;\wedge\; TendstoInMeasure(μ, f\circ ns, atTop, g).$$$

Lean4

theorem exists_seq_tendstoInMeasure_atTop {u : Filter ι} [NeBot u] [IsCountablyGenerated u] {f : ι → α → E} {g : α → E}
    (hfg : TendstoInMeasure μ f u g) :
    ∃ ns : ℕ → ι, Tendsto ns atTop u ∧ TendstoInMeasure μ (fun n => f (ns n)) atTop g :=
  by
  obtain ⟨ns, h_tendsto_ns⟩ : ∃ ns : ℕ → ι, Tendsto ns atTop u := exists_seq_tendsto u
  exact ⟨ns, h_tendsto_ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩

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