seqTendstoAeSeq — Mathlib

English

From a TendstoInMeasure relation, define a strictly increasing subsequence sequence that witnesses almost-everywhere convergence of a subsequence.

Русский

Из отношения TendstoInMeasure задайте строго возрастающую подпоследовательность, которая демонстрирует почти везде сходимость подпоследовательности.

LaTeX

$$$\text{Let } hfg: TendstoInMeasure(\mu,f,atTop,g). \text{ Then } seqTendstoAeSeq(hfg):\mathbb{N}\to\mathbb{N} \text{ is strictly increasing and ... }$$$

Lean4

/-- Transformation of `seqTendstoAeSeqAux` to makes sure it is strictly monotone. -/
noncomputable def seqTendstoAeSeq (hfg : TendstoInMeasure μ f atTop g) : ℕ → ℕ
  | 0 => seqTendstoAeSeqAux hfg 0
  | n + 1 => max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)

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