sfiniteSeq_absolutelyContinuous_toFinite

English

For μ, n, sfiniteSeq μ n ≪ μ.toFinite; each term is absolutely continuous with respect to the finite version.

Русский

Для μ, n: sfiniteSeq μ n ≪ μ.toFinite; каждый элемент несёт абсолютную непрерывность по отношению к конечной версии.

LaTeX

$$$ sfiniteSeq(\mu,n) \ll μ^{toFinite} $$$

Lean4

theorem sfiniteSeq_absolutelyContinuous_toFinite (μ : Measure α) [SFinite μ] (n : ℕ) : sfiniteSeq μ n ≪ μ.toFinite :=
  (sfiniteSeq_le μ n).absolutelyContinuous.trans (absolutelyContinuous_toFinite μ)

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