IicSnd_ac_fst

Mathlib.Probability.Kernel.Disintegration.CondCDF

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.IicSnd_ac_fst

English

IicSnd r is absolutely continuous with respect to fst.

Русский

IicSnd r абсолютно непрерывна относительно fst.

LaTeX

$$$IicSnd(r) \ll ρ.fst$$$

Lean4

theorem IicSnd_ac_fst (r : ℝ) : ρ.IicSnd r ≪ ρ.fst :=
  Measure.absolutelyContinuous_of_le (IicSnd_le_fst ρ r)

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

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

Разделы

Аффилиация

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