English
For NNReal r with r ≠ 0, ν.rnDeriv (r • μ) equals ν.rnDeriv μ scaled by r⁻¹ almost everywhere: ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ.
Русский
Для NNReal r, r ≠ 0, производная ν по (r • μ) равна r⁻¹ умноженной на ν.rnDeriv μ почти наверняка.
LaTeX
$$$ r\\neq 0 \\Rightarrow ν.rnDeriv (r·μ) =ᵐ[μ] r^{-1} · (ν.rnDeriv μ) $$$
Lean4
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right'`, which requires sigma-finite `ν` and `μ`. -/
theorem rnDeriv_smul_right (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {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]
rotate_left
· exact (measurable_rnDeriv _ _).aemeasurable
· exact (measurable_rnDeriv _ _).aemeasurable.const_smul _
· exact (lintegral_rnDeriv_lt_top ν _).ne
· 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 μ
