rnDeriv_sub — Mathlib

English

Under Lebesgue decompositions, the RN-derivative of s − t equals s.rnDeriv μ minus t.rnDeriv μ almost everywhere.

Русский

При разложениях Лебега производная RN от s − t равна произведенной разности rnDeriv s и rnDeriv t почти наверняка.

LaTeX

$$$ (s - t).rnDeriv \\mu =^{{\\mu}}_{a.e.} s.rnDeriv \\mu - t.rnDeriv \\mu $$$

Lean4

theorem rnDeriv_sub (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    [t.HaveLebesgueDecomposition μ] [hst : (s - t).HaveLebesgueDecomposition μ] :
    (s - t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ - t.rnDeriv μ :=
  by
  rw [sub_eq_add_neg] at hst
  rw [sub_eq_add_neg, sub_eq_add_neg]
  grw [rnDeriv_add, rnDeriv_neg]

Похожие утверждения