haveLebesgueDecomposition

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

English

If μ ⟂ₘ ν, then μ have Lebesgue decomposition with respect to ν.

Русский

Если μ взаимно сингулярна ν, то μ имеет разложение Лебега по ν.

LaTeX

$$μ ⟂ₘ ν → HaveLebesgueDecomposition μ ν$$

Lean4

theorem haveLebesgueDecomposition (h : μ ⟂ₘ ν) : HaveLebesgueDecomposition μ ν :=
  ⟨⟨(μ, 0), measurable_zero, h, by simp⟩⟩

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

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

Разделы

Аффилиация

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