absolutelyContinuous_toFinite

Mathlib.MeasureTheory.Measure.WithDensityFinite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.absolutelyContinuous_toFinite

English

μ ≪ μ.toFinite: μ is absolutely continuous with respect to its finite version when μ is SFinite.

Русский

μ ∥ μ.toFinite: μ абсолютно непрерывна относительно своей конечной версии при μ ∈ SFinite.

LaTeX

$$$ μ \ll μ^{toFinite} $$$

Lean4

theorem absolutelyContinuous_toFinite (μ : Measure α) [SFinite μ] : μ ≪ μ.toFinite :=
  Measure.ae_le_iff_absolutelyContinuous.mp ae_toFinite.ge

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru