English
For ENNReal-scaled μ and with ν finite etc., if r ≠ 0 and r ≠ ∞, then ν.rnDeriv (r•μ) =ᵐ μ r⁻¹ • ν.rnDeriv μ.
Русский
Если r ≠ 0, r ≠ ∞, то RN-производная ν по отношению к r·μ равна a.e. μ произведению r⁻¹ и RN-производной ν по отношению к μ.
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`, which has no hypothesis on `μ` but requires finite `ν`. -/
theorem rnDeriv_smul_right' (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ℝ≥0} (hr : r ≠ 0) :
ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ :=
by
refine
(absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)
rw [← withDensity_eq_iff_of_sigmaFinite]
· simp_rw [ENNReal.smul_def]
rw [withDensity_smul _ (measurable_rnDeriv _ _)]
suffices
ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ)) =
ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ)
by rwa [add_right_inj] at this
rw [← ν.haveLebesgueDecomposition_add (r • μ), singularPart_smul_right _ _ _ hr, ENNReal.smul_def r,
withDensity_smul_measure, ← ENNReal.smul_def, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀ hr, one_smul]
exact ν.haveLebesgueDecomposition_add μ
· exact (measurable_rnDeriv _ _).aemeasurable
· exact (measurable_rnDeriv _ _).aemeasurable.const_smul _
