English
For two finite measures ν1 and ν2, the Radon–Nikodym derivative of their sum with respect to μ equals the sum of their RN derivatives with respect to μ, almost everywhere (with respect to μ).
Русский
Для двух конечных мер ν1 и ν2 радоновская производная их суммы по отношению к μ равна сумме их радоновских производных по отношению к μ почти наверняка.
LaTeX
$$$$ (\\nu_1 + \\nu_2)\\mathrm{rnDeriv}\\mu =^{a.e.}_{\\mu} \\nu_1\\mathrm{rnDeriv}\\mu + \\nu_2\\mathrm{rnDeriv}\\mu $$$$
Lean4
/-- Radon-Nikodym derivative of a sum of two measures.
See also `rnDeriv_add'`, which requires sigma-finite `ν₁`, `ν₂` and `μ`. -/
theorem rnDeriv_add (ν₁ ν₂ μ : Measure α) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ]
[ν₂.HaveLebesgueDecomposition μ] [(ν₁ + ν₂).HaveLebesgueDecomposition μ] :
(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ :=
by
rw [← withDensity_eq_iff]
· suffices
(ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
(ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
by rwa [add_right_inj] at this
rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add, withDensity_add_left (measurable_rnDeriv _ _),
add_assoc, add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ), ←
ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
· exact (measurable_rnDeriv _ _).aemeasurable
· exact ((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable
· exact (lintegral_rnDeriv_lt_top (ν₁ + ν₂) μ).ne
