instIsFiniteMeasure

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

← MathLib Explorer

English

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

Русский

Если μ конечна, то ν.withDensity(μ.rnDer ν) конечна.

LaTeX

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

Lean4

instance instIsFiniteMeasure [IsFiniteMeasure μ] : IsFiniteMeasure (ν.withDensity <| μ.rnDeriv ν) :=
  isFiniteMeasure_of_le μ <| withDensity_rnDeriv_le μ ν

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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