α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
this :
  toJordanDecomposition (singularPart s μ) =
    JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
      (Measure.singularPart (toJordanDecomposition s).negPart μ)
      (_ :
        Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
          Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ totalVariation (singularPart s μ) =
    Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ totalVariation (singularPart s μ) =
    Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ
have :
  (s.singularPart μ).toJordanDecomposition =
    ⟨s.toJordanDecomposition.posPart.singularPart μ,
      s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by
  refine' JordanDecomposition.toSignedMeasure_injective _
  rw [toSignedMeasure_toJordanDecomposition]
  rfl
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ JordanDecomposition.toSignedMeasure (toJordanDecomposition (singularPart s μ)) =
    JordanDecomposition.toSignedMeasure
      (JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
        (Measure.singularPart (toJordanDecomposition s).negPart μ)
        (_ :
          Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
            Measure.singularPart (toJordanDecomposition s).negPart μ))
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ toJordanDecomposition (singularPart s μ) =
    JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
      (Measure.singularPart (toJordanDecomposition s).negPart μ)
      (_ :
        Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
          Measure.singularPart (toJordanDecomposition s).negPart μ)
refine' JordanDecomposition.toSignedMeasure_injective _
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ singularPart s μ =
    JordanDecomposition.toSignedMeasure
      (JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
        (Measure.singularPart (toJordanDecomposition s).negPart μ)
        (_ :
          Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
            Measure.singularPart (toJordanDecomposition s).negPart μ))
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ JordanDecomposition.toSignedMeasure (toJordanDecomposition (singularPart s μ)) =
    JordanDecomposition.toSignedMeasure
      (JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
        (Measure.singularPart (toJordanDecomposition s).negPart μ)
        (_ :
          Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
            Measure.singularPart (toJordanDecomposition s).negPart μ))
rw [toSignedMeasure_toJordanDecomposition]
no goals
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ singularPart s μ =
    JordanDecomposition.toSignedMeasure
      (JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
        (Measure.singularPart (toJordanDecomposition s).negPart μ)
        (_ :
          Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
            Measure.singularPart (toJordanDecomposition s).negPart μ))
rfl
no goals
α : Type u_1
β : Type ?u.301151
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
this :
  toJordanDecomposition (singularPart s μ) =
    JordanDecomposition.mk (Measure.singularPart (toJordanDecomposition s).posPart μ)
      (Measure.singularPart (toJordanDecomposition s).negPart μ)
      (_ :
        Measure.singularPart (toJordanDecomposition s).posPart μ ⟂ₘ
          Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ totalVariation (singularPart s μ) =
    Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ
rw [totalVariation, this]