{α : Type u_2} →
  [inst : MeasurableSpace α] →
    (posPart negPart : MeasureTheory.Measure α) →
      [posPart_finite : MeasureTheory.IsFiniteMeasure posPart] →
        [negPart_finite : MeasureTheory.IsFiniteMeasure negPart] →
          posPart.MutuallySingular negPart → MeasureTheory.JordanDecomposition α