English
If s is a Hahn decomposition for μ and ν, then restricting ν − μ to s yields the difference of the restricted signed measures: ((ν − μ).restrict s).toSignedMeasure = ν.toSignedMeasure.restrict s − μ.toSignedMeasure.restrict s.
Русский
Пусть s является разложением Хана для μ и ν; ограничение ν − μ до s равно разности ограниченных знаковых мер: ((ν − μ).restrict s).toSignedMeasure = ν.toSignedMeasure.restrict s − μ.toSignedMeasure.restrict s.
LaTeX
$$$((\nu - \mu) \restriction s)^{\text{toSignedMeasure}} = \nu^{\text{toSignedMeasure}} \restriction s - \mu^{\text{toSignedMeasure}} \restriction s$$$
Lean4
theorem toSignedMeasure_restrict_sub (hs : IsHahnDecomposition μ ν s) :
((ν - μ).restrict s).toSignedMeasure = ν.toSignedMeasure.restrict s - μ.toSignedMeasure.restrict s :=
by
have hmeas := hs.measurableSet
rw [eq_sub_iff_add_eq, toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas, ← toSignedMeasure_add]
simp only [restrict_sub_eq_restrict_sub_restrict, hmeas, sub_add_cancel_of_le hs.le_on]
exact (toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas).symm
