English
The RN derivative scales under left scalar multiplication: (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ.
Русский
RN-дериватив масштабируется слева при умножении на число: (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ.
LaTeX
$$$ (r\\cdot ν).rnDeriv μ =ᵐ[μ] r \\cdot (ν.rnDeriv μ) $$$
Lean4
/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left'`, which requires sigma-finite `ν` and `μ`. -/
theorem rnDeriv_smul_left (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] (r : ℝ≥0) :
(r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ := by
rw [← withDensity_eq_iff]
· simp_rw [ENNReal.smul_def]
rw [withDensity_smul _ (measurable_rnDeriv _ _)]
suffices
(r • ν).singularPart μ + withDensity μ (rnDeriv (r • ν) μ) =
(r • ν).singularPart μ + r • withDensity μ (rnDeriv ν μ)
by rwa [Measure.add_right_inj] at this
rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add, ← ν.haveLebesgueDecomposition_add μ]
· exact (measurable_rnDeriv _ _).aemeasurable
· exact (measurable_rnDeriv _ _).aemeasurable.const_smul _
· exact (lintegral_rnDeriv_lt_top (r • ν) μ).ne
