α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
⊢ withDensityᵥ μ (rnDeriv s μ) = s

α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : totalVariation s ≪ ennrealToMeasure (toENNRealVectorMeasure μ)
⊢ ennrealToMeasure (toENNRealVectorMeasure μ) = μ
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s ≪ᵥ toENNRealVectorMeasure μ
⊢ withDensityᵥ μ (rnDeriv s μ) = s
rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
  totalVariation_absolutelyContinuous_iff] at h
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (rnDeriv s μ)) i = ↑s i
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
⊢ withDensityᵥ μ (rnDeriv s μ) = s
ext1 i hi
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑(toJordanDecomposition s).posPart i) - ENNReal.toReal (↑↑(toJordanDecomposition s).negPart i) = ↑s i

case h.hf
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).posPart μ x)

case h.hg
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (rnDeriv s μ)) i = ↑s i
rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv, integral_sub,
  withDensity_rnDeriv_toReal_eq h.1 hi, withDensity_rnDeriv_toReal_eq h.2 hi]
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑(toJordanDecomposition s).posPart i) - ENNReal.toReal (↑↑(toJordanDecomposition s).negPart i) =
    ↑(JordanDecomposition.toSignedMeasure (toJordanDecomposition s)) i
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑(toJordanDecomposition s).posPart i) - ENNReal.toReal (↑↑(toJordanDecomposition s).negPart i) = ↑s i
conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑(toJordanDecomposition s).posPart i) - ENNReal.toReal (↑↑(toJordanDecomposition s).negPart i) =
    ↑(toSignedMeasure (toJordanDecomposition s).posPart) i - ↑(toSignedMeasure (toJordanDecomposition s).negPart) i
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑(toJordanDecomposition s).posPart i) - ENNReal.toReal (↑↑(toJordanDecomposition s).negPart i) =
    ↑(JordanDecomposition.toSignedMeasure (toJordanDecomposition s)) i
erw [VectorMeasure.sub_apply]
no goals
case h
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ENNReal.toReal (↑↑(toJordanDecomposition s).posPart i) - ENNReal.toReal (↑↑(toJordanDecomposition s).negPart i) =
    ↑(toSignedMeasure (toJordanDecomposition s).posPart) i - ↑(toSignedMeasure (toJordanDecomposition s).negPart) i
rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi]
case h.hg
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)) Set.univ
case h.hg
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
rw [← integrableOn_univ]
case h.hg
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)) Set.univ
case h.hg
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)) Set.univ
refine' IntegrableOn.restrict _ MeasurableSet.univ
case h.hg.refine'_1
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x))
    (Measure.restrict μ Set.univ)

case h.hg.refine'_2
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in Set.univ, Measure.rnDeriv (toJordanDecomposition s).negPart μ x ∂μ) ≠ ⊤
case h.hg
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)) Set.univ
refine' ⟨_, hasFiniteIntegral_toReal_of_lintegral_ne_top _⟩
case h.hg.refine'_1.hf
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Measurable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
case h.hg.refine'_1
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ AEStronglyMeasurable (fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x))
    (Measure.restrict μ Set.univ)
apply Measurable.aestronglyMeasurable
no goals
case h.hg.refine'_1.hf
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Measurable fun x => ENNReal.toReal (Measure.rnDeriv (toJordanDecomposition s).negPart μ x)
measurability
case h.hg.refine'_2
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α), Measure.rnDeriv (toJordanDecomposition s).negPart μ x ∂μ) ≠ ⊤
case h.hg.refine'_2
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in Set.univ, Measure.rnDeriv (toJordanDecomposition s).negPart μ x ∂μ) ≠ ⊤
rw [set_lintegral_univ]
no goals
case h.hg.refine'_2
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α), Measure.rnDeriv (toJordanDecomposition s).negPart μ x ∂μ) ≠ ⊤
exact (lintegral_rnDeriv_lt_top _ _).ne
no goals
α : Type u_1
β : Type ?u.4814
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : totalVariation s ≪ ennrealToMeasure (toENNRealVectorMeasure μ)
⊢ ennrealToMeasure (toENNRealVectorMeasure μ) = μ
exact equivMeasure.right_inv μ