rnDeriv_smul — Mathlib

English

For a real number r, the RN-derivative of r·s is almost everywhere r times the RN-derivative of s with respect to μ.

Русский

Для вещественного коэффициента r производная Радона–Никодымова от r·s равна почти наверняка r умноженной на RN-дериватив s.

LaTeX

$$$ (r \\cdot s).rnDeriv \\mu =^{{\\mu}}_{a.e.} r \\cdot s.rnDeriv \\mu $$$

Lean4

theorem rnDeriv_smul (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] (r : ℝ) :
    (r • s).rnDeriv μ =ᵐ[μ] r • s.rnDeriv μ :=
  by
  refine Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) ((integrable_rnDeriv _ _).smul r) ?_
  rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add, singularPart_add_withDensity_rnDeriv_eq]

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