jordanDecompositionOfToSignedMeasureSub

Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

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

Lean4

/-- The Jordan decomposition associated to the pair of mutually singular measures `μ - ν`
and `ν - μ`. -/
def jordanDecompositionOfToSignedMeasureSub (μ ν : Measure X) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    JordanDecomposition X where
  posPart := μ - ν
  negPart := ν - μ
  mutuallySingular := mutually_singular_measure_sub

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

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

Разделы

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

Аффилиация

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