α : Type u_1
β : Type ?u.303346
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x =>
    ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).posPart μ x) -
      ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
α : Type u_1
β : Type ?u.303346
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measurable (rnDeriv s μ)
rw [rnDeriv]
no goals
α : Type u_1
β : Type ?u.303346
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x =>
    ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).posPart μ x) -
      ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
measurability