α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff] at htμ
α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
change
  _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) ∧
    _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ
α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
rw [VectorMeasure.equivMeasure.right_inv] at htμ
no goals
α : Type u_1
β : Type ?u.449524
m : MeasurableSpace α
μ ν : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ ((toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ
    (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
exact
  ((JordanDecomposition.mutuallySingular _).add_right
        (htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
    ((htμ.2.symm.mono_ac (withDensity_absolutelyContinuous _ _) (refl _)).add_right
      (withDensity_ofReal_mutuallySingular hf))