α : Type u_1
β : Type ?u.655633
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
hst : HaveLebesgueDecomposition (s + -t) μ
⊢ rnDeriv (s - t) μ =ᶠ[ae μ] rnDeriv s μ - rnDeriv t μ
α : Type u_1
β : Type ?u.655633
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
hst : HaveLebesgueDecomposition (s - t) μ
⊢ rnDeriv (s - t) μ =ᶠ[ae μ] rnDeriv s μ - rnDeriv t μ
rw [sub_eq_add_neg] at hst
α : Type u_1
β : Type ?u.655633
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
hst : HaveLebesgueDecomposition (s + -t) μ
⊢ rnDeriv (s + -t) μ =ᶠ[ae μ] rnDeriv s μ + -rnDeriv t μ
α : Type u_1
β : Type ?u.655633
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
hst : HaveLebesgueDecomposition (s + -t) μ
⊢ rnDeriv (s - t) μ =ᶠ[ae μ] rnDeriv s μ - rnDeriv t μ
rw [sub_eq_add_neg, sub_eq_add_neg]
no goals
α : Type u_1
β : Type ?u.655633
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
hst : HaveLebesgueDecomposition (s + -t) μ
⊢ rnDeriv (s + -t) μ =ᶠ[ae μ] rnDeriv s μ + -rnDeriv t μ
exact ae_eq_trans (rnDeriv_add _ _ _) (Filter.EventuallyEq.add (ae_eq_refl _) (rnDeriv_neg _ _))