English
Let ν and μ be finite measures on a measurable space, and let r be a positive finite scalar. Then the Radon–Nikodym derivative of ν with respect to r·μ is almost everywhere equal (with respect to μ) to r^{-1} times the Radon–Nikodym derivative of ν with respect to μ.
Русский
Пусть ν и μ — конечные меры на измеримое пространство, и пусть r — положительное конечное число. Тогда радонникова производная ν по отношению к r·μ равна почти всюду (по μ) r^{-1} умноженной на радонникову производную ν по отношению к μ.
LaTeX
$$$$ \\nu\\mathrm{rnDeriv}(r\\mu) =^{a.e.}_{\\mu} r^{-1} \\cdot \\nu\\mathrm{rnDeriv}(\\mu) $$$$
Lean4
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right_of_ne_top'`, which requires sigma-finite `ν` and `μ`. -/
theorem rnDeriv_smul_right_of_ne_top (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : ℝ≥0∞}
(hr : r ≠ 0) (hr_ne_top : r ≠ ∞) : ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ :=
by
have h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ :=
by
refine rnDeriv_smul_right ν μ ?_
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
simp [hr, hr_ne_top]
have : (r.toNNReal)⁻¹ • rnDeriv ν μ = r⁻¹ • rnDeriv ν μ :=
by
ext x
simp only [Pi.smul_apply, ENNReal.smul_def, smul_eq_mul]
rw [ENNReal.coe_inv, ENNReal.coe_toNNReal hr_ne_top]
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
simp [hr, hr_ne_top]
simp_rw [this, ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top] at h
exact h
