English
For a signed measure s and μ with Lebesgue decomposition, RN-derivative respect scaling: (r · s).rnDeriv μ =^{{μ}}_{a.e.} r · s.rnDeriv μ.
Русский
Для знаковой меры s и μ с разложением Лебега производная RN respects масштабирование: (r·s).rnDeriv μ = a.e. (r·s.rnDeriv μ).
LaTeX
$$$ (r \\cdot s).rnDeriv μ =^{{\\mu}}_{a.e.} r \\cdot s.rnDeriv μ $$$
Lean4
theorem withDensityᵥ_rnDeriv_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ ν : Measure α}
[μ.HaveLebesgueDecomposition ν] [SigmaFinite μ] {f : α → E} (hμν : μ ≪ ν) (hf : Integrable f μ) :
ν.withDensityᵥ (fun x ↦ (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f := by
rw [withDensityᵥ_smul_eq_withDensityᵥ_withDensity' (measurable_rnDeriv μ ν).aemeasurable (rnDeriv_lt_top μ ν)
((integrable_rnDeriv_smul_iff hμν).mpr hf),
withDensity_rnDeriv_eq μ ν hμν]