rnDeriv_neg — Mathlib

English

The Radon–Nikodym derivative of the negated signed measure equals the negative of the Radon–Nikodym derivative, almost everywhere.

Русский

Рациональная производная от отрицательной знаковой меры равна минус производной от исходной меры почти наверняка.

LaTeX

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

Lean4

theorem rnDeriv_neg (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] :
    (-s).rnDeriv μ =ᵐ[μ] -s.rnDeriv μ :=
  by
  refine Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) (integrable_rnDeriv _ _).neg ?_
  rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    singularPart_neg, ← neg_add, singularPart_add_withDensity_rnDeriv_eq]

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