α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
⊢ f =ᶠ[ae μ] rnDeriv s μ
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ f =ᶠ[ae μ] rnDeriv s μ
set f' := hfi.1.mk f
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
hadd' : s = t + withDensityᵥ μ f'
⊢ f =ᶠ[ae μ] rnDeriv s μ
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
⊢ f =ᶠ[ae μ] rnDeriv s μ
have hadd' : s = t + μ.withDensityᵥ f' := by
  convert hadd using 2
  exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
hadd' : s = t + withDensityᵥ μ f'
this : HaveLebesgueDecomposition s μ
⊢ f =ᶠ[ae μ] rnDeriv s μ
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
hadd' : s = t + withDensityᵥ μ f'
⊢ f =ᶠ[ae μ] rnDeriv s μ
haveI := haveLebesgueDecomposition_mk μ hfi.1.measurable_mk htμ hadd'
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
hadd' : s = t + withDensityᵥ μ f'
this : HaveLebesgueDecomposition s μ
⊢ withDensityᵥ μ (rnDeriv s μ) = withDensityᵥ μ f
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
hadd' : s = t + withDensityᵥ μ f'
this : HaveLebesgueDecomposition s μ
⊢ f =ᶠ[ae μ] rnDeriv s μ
refine' (Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) hfi _).symm
no goals
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
hadd' : s = t + withDensityᵥ μ f'
this : HaveLebesgueDecomposition s μ
⊢ withDensityᵥ μ (rnDeriv s μ) = withDensityᵥ μ f
rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
  singularPart_add_withDensity_rnDeriv_eq]
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
⊢ withDensityᵥ μ f' = withDensityᵥ μ f
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
⊢ s = t + withDensityᵥ μ f'
convert hadd using 2
no goals
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.641648
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
f' : α → ℝ := AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)
⊢ withDensityᵥ μ f' = withDensityᵥ μ f
exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm