seqTendstoAeSeqAux — Mathlib

English

From a TendstoInMeasure relation, one can select a sequence N_n such that the bound holds for each n, defining an auxiliary subsequence sequence.

Русский

Из отношения сходности по мере можно выбрать последовательность N_n так, чтобы для каждого n выполнялось требование, задающее вспомогательную подпоследовательность.

LaTeX

$$$\text{Given } hfg: TendstoInMeasure(\mu,f,atTop,g), \exists N:\mathbb{N} \to \mathbb{N},\; \text{...}$$$

Lean4

/-- Given a sequence of functions `f` which converges in measure to `g`,
`seqTendstoAeSeqAux` is a sequence such that
`∀ m ≥ seqTendstoAeSeqAux n, μ {x | 2⁻¹ ^ n ≤ dist (f m x) (g x)} ≤ 2⁻¹ ^ n`. -/
noncomputable def seqTendstoAeSeqAux (hfg : TendstoInMeasure μ f atTop g) (n : ℕ) :=
  Classical.choose (exists_nat_measure_lt_two_inv hfg n)

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