[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
⊢ withDensity ν (rnDeriv μ ν) = μ
[PROOFSTEP]
obtain ⟨_, ⟨E, hE₁, hE₂, hE₃⟩, hadd⟩ := haveLebesgueDecomposition_spec μ ν
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
[PROOFSTEP]
have : singularPart μ ν = 0 :=
  by
  refine' le_antisymm (fun A (_ : MeasurableSet A) => _) (Measure.zero_le _)
  suffices singularPart μ ν Set.univ = 0
    by
    rw [Measure.coe_zero, Pi.zero_apply, ← this]
    exact measure_mono (Set.subset_univ _)
  rw [← measure_add_measure_compl hE₁, hE₂, zero_add]
  have : (singularPart μ ν + ν.withDensity (rnDeriv μ ν)) Eᶜ = μ Eᶜ := by rw [← hadd]
  rw [Measure.coe_add, Pi.add_apply, h hE₃] at this
  exact (add_eq_zero_iff.1 this).1
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
⊢ singularPart μ ν = 0
[PROOFSTEP]
refine' le_antisymm (fun A (_ : MeasurableSet A) => _) (Measure.zero_le _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑0 A
[PROOFSTEP]
suffices singularPart μ ν Set.univ = 0
  by
  rw [Measure.coe_zero, Pi.zero_apply, ← this]
  exact measure_mono (Set.subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) Set.univ = 0
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑0 A
[PROOFSTEP]
rw [Measure.coe_zero, Pi.zero_apply, ← this]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) Set.univ = 0
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑(singularPart μ ν) Set.univ
[PROOFSTEP]
exact measure_mono (Set.subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) Set.univ = 0
[PROOFSTEP]
rw [← measure_add_measure_compl hE₁, hE₂, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) Eᶜ = 0
[PROOFSTEP]
have : (singularPart μ ν + ν.withDensity (rnDeriv μ ν)) Eᶜ = μ Eᶜ := by rw [← hadd]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν + withDensity ν (rnDeriv μ ν)) Eᶜ = ↑↑μ Eᶜ
[PROOFSTEP]
rw [← hadd]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν + withDensity ν (rnDeriv μ ν)) Eᶜ = ↑↑μ Eᶜ
⊢ ↑↑(singularPart μ ν) Eᶜ = 0
[PROOFSTEP]
rw [Measure.coe_add, Pi.add_apply, h hE₃] at this
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) Eᶜ + ↑↑(withDensity ν (rnDeriv μ ν)) Eᶜ = 0
⊢ ↑↑(singularPart μ ν) Eᶜ = 0
[PROOFSTEP]
exact (add_eq_zero_iff.1 this).1
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
this : singularPart μ ν = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
[PROOFSTEP]
rw [this, zero_add] at hadd
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν Eᶜ = 0
this : singularPart μ ν = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
[PROOFSTEP]
exact hadd.symm
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, ENNReal.toReal (rnDeriv μ ν x) ∂ν = ENNReal.toReal (↑↑μ i)
[PROOFSTEP]
rw [integral_toReal, ← withDensity_apply _ hi, withDensity_rnDeriv_eq μ ν h]
[GOAL]
case hfm
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ AEMeasurable fun x => rnDeriv μ ν x
[PROOFSTEP]
measurability
[GOAL]
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂restrict ν i, rnDeriv μ ν x < ⊤
[PROOFSTEP]
refine' ae_lt_top (μ.measurable_rnDeriv ν) (lt_of_le_of_lt (lintegral_mono_set i.subset_univ) _).ne
[GOAL]
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in Set.univ, rnDeriv μ ν x ∂ν < ⊤
[PROOFSTEP]
rw [← withDensity_apply _ MeasurableSet.univ, withDensity_rnDeriv_eq μ ν h]
[GOAL]
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
i : Set α
hi : MeasurableSet i
⊢ ↑↑μ Set.univ < ⊤
[PROOFSTEP]
exact measure_lt_top _ _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s ≪ᵥ toENNRealVectorMeasure μ
⊢ withDensityᵥ μ (rnDeriv s μ) = s
[PROOFSTEP]
rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
  totalVariation_absolutelyContinuous_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
⊢ withDensityᵥ μ (rnDeriv s μ) = s
[PROOFSTEP]
ext1 i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv, integral_sub, withDensity_rnDeriv_toReal_eq h.1 hi,
  withDensity_rnDeriv_toReal_eq h.2 hi]
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
| ↑s i
[PROOFSTEP]
rw [← s.toSignedMeasure_toJordanDecomposition]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
| ↑s i
[PROOFSTEP]
rw [← s.toSignedMeasure_toJordanDecomposition]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
| ↑s i
[PROOFSTEP]
rw [← s.toSignedMeasure_toJordanDecomposition]
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
erw [VectorMeasure.sub_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi]
[GOAL]
case h.hf
α : Type u_1
β : Type u_2
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_2
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)
[PROOFSTEP]
all_goals
  rw [← integrableOn_univ]
  refine' IntegrableOn.restrict _ MeasurableSet.univ
  refine' ⟨_, hasFiniteIntegral_toReal_of_lintegral_ne_top _⟩
  · apply Measurable.aestronglyMeasurable
    measurability
  · rw [set_lintegral_univ]
    exact (lintegral_rnDeriv_lt_top _ _).ne
[GOAL]
case h.hf
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rw [← integrableOn_univ]
[GOAL]
case h.hf
α : Type u_1
β : Type u_2
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).posPart μ x)) Set.univ
[PROOFSTEP]
refine' IntegrableOn.restrict _ MeasurableSet.univ
[GOAL]
case h.hf
α : Type u_1
β : Type u_2
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).posPart μ x)) Set.univ
[PROOFSTEP]
refine' ⟨_, hasFiniteIntegral_toReal_of_lintegral_ne_top _⟩
[GOAL]
case h.hf.refine'_1
α : Type u_1
β : Type u_2
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).posPart μ x))
    (Measure.restrict μ Set.univ)
[PROOFSTEP]
apply Measurable.aestronglyMeasurable
[GOAL]
case h.hf.refine'_1.hf
α : Type u_1
β : Type u_2
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).posPart μ x)
[PROOFSTEP]
measurability
[GOAL]
case h.hf.refine'_2
α : Type u_1
β : Type u_2
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).posPart μ x ∂μ ≠ ⊤
[PROOFSTEP]
rw [set_lintegral_univ]
[GOAL]
case h.hf.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α), Measure.rnDeriv (toJordanDecomposition s).posPart μ x ∂μ ≠ ⊤
[PROOFSTEP]
exact (lintegral_rnDeriv_lt_top _ _).ne
[GOAL]
case h.hg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rw [← integrableOn_univ]
[GOAL]
case h.hg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' IntegrableOn.restrict _ MeasurableSet.univ
[GOAL]
case h.hg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' ⟨_, hasFiniteIntegral_toReal_of_lintegral_ne_top _⟩
[GOAL]
case h.hg.refine'_1
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
apply Measurable.aestronglyMeasurable
[GOAL]
case h.hg.refine'_1.hf
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
measurability
[GOAL]
case h.hg.refine'_2
α : Type u_1
β : Type u_2
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 ∂μ ≠ ⊤
[PROOFSTEP]
rw [set_lintegral_univ]
[GOAL]
case h.hg.refine'_2
α : Type u_1
β : Type u_2
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 ∂μ ≠ ⊤
[PROOFSTEP]
exact (lintegral_rnDeriv_lt_top _ _).ne
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : totalVariation s ≪ ennrealToMeasure (toENNRealVectorMeasure μ)
⊢ ennrealToMeasure (toENNRealVectorMeasure μ) = μ
[PROOFSTEP]
exact equivMeasure.right_inv μ