English
If μ has Lebesgue decomposition w.r.t. ν and μ ≪ ν, then the RN-derivative ν rnDeriv ν with respect to μ is almost everywhere positive.
Русский
Если μ имеет разложение Лебеса по ν и μ эквивалентно ν (μ ≪ ν), то радоновская производная ν по отношению к μ положительна почти всюду по μ.
LaTeX
$$$$ \\text{ae}_{\\mu}(x): 0 < \\nu\\mathrm{rnDeriv}(ν, μ)(x) \\,. $$$$
Lean4
/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left`, which has no hypothesis on `μ` but requires finite `ν`. -/
theorem rnDeriv_smul_left' (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] (r : ℝ≥0) :
(r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ :=
by
rw [← withDensity_eq_iff_of_sigmaFinite]
· 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 _
