instSigmaFinite

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

English

If μ is sigma-finite, then ν.withDensity(μ.rnDer ν) is sigma-finite.

Русский

Если μ сигма-финитна, то ν.withDensity(μ.rnDer ν) сигма-финитна.

LaTeX

$$$$ [SigmaFinite μ] \Rightarrow SigmaFinite(ν.withDensity(μ.rnDer ν)) $$$$

Lean4

instance instSigmaFinite [SigmaFinite μ] : SigmaFinite (ν.withDensity <| μ.rnDeriv ν) :=
  sigmaFinite_of_le μ <| withDensity_rnDeriv_le μ ν

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

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

Разделы

Аффилиация

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