case pos
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
⊢ singularPart (r • s) μ = r • singularPart s μ

case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ singularPart (r • s) μ = r • singularPart s μ
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
⊢ singularPart (r • s) μ = r • singularPart s μ
by_cases hr : 0 ≤ r
case pos.intro
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ singularPart (↑r • s) μ = ↑r • singularPart s μ
case pos
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
⊢ singularPart (r • s) μ = r • singularPart s μ
lift r to ℝ≥0 using hr
no goals
case pos.intro
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ singularPart (↑r • s) μ = ↑r • singularPart s μ
exact singularPart_smul_nnreal s μ r
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ toSignedMeasure (Measure.singularPart (toJordanDecomposition (r • s)).posPart μ) -
      toSignedMeasure (Measure.singularPart (toJordanDecomposition (r • s)).negPart μ) =
    r •
      (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
        toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ singularPart (r • s) μ = r • singularPart s μ
rw [singularPart, singularPart]
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ -(Real.toNNReal (-r) •
        (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
          toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))) =
    r •
      (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
        toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ toSignedMeasure (Real.toNNReal (-r) • Measure.singularPart (toJordanDecomposition s).negPart μ) -
      toSignedMeasure (Real.toNNReal (-r) • Measure.singularPart (toJordanDecomposition s).posPart μ) =
    r •
      (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
        toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))
rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub]
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ -(↑(Real.toNNReal (-r)) •
        (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
          toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))) =
    r •
      (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
        toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ -(Real.toNNReal (-r) •
        (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
          toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))) =
    r •
      (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
        toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))
change -(((-r).toNNReal : ℝ) • (_ : SignedMeasure α)) = _
no goals
case neg
α : Type u_1
β : Type ?u.630886
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
r : ℝ
hr : ¬0 ≤ r
⊢ -(↑(Real.toNNReal (-r)) •
        (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
          toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))) =
    r •
      (toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
        toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ))
rw [← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr (not_le.1 hr))), neg_neg]