case refine'_2.left
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)) μ

case refine'_2.right
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ HasFiniteIntegral fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
case refine'_2
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Integrable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
constructor
no goals
case refine'_2.right
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ HasFiniteIntegral fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
exact hasFiniteIntegral_toReal_of_lintegral_ne_top (lintegral_rnDeriv_lt_top _ μ).ne
case refine'_2.left.hf
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
case refine'_2.left
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)) μ
apply Measurable.aestronglyMeasurable
no goals
case refine'_2.left.hf
α : Type u_1
β : Type ?u.376607
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
measurability