English
Suppose t is mutually singular with μ and s = t + μ.withDensityᵥ f for some function f integrable with respect to μ. Then f is the Radon–Nikodym derivative of s with respect to μ (μ-almost everywhere).
Русский
Пусть t обособлена от μ, и что s = t + μ.withDensityᵥ f для некоторой функции f, интегрируемой по μ. Тогда f является радоново-никодымовым производным s по отношению к μ (почти по μ).
LaTeX
$$$ f =^{{\\mu}}_{a.e.} s.rnDeriv \\mu $$$
Lean4
/-- Given a measure `μ`, signed measures `s` and `t`, and a function `f` such that `t` is
mutually singular with respect to `μ` and `s = t + μ.withDensityᵥ f`, we have
`f = rnDeriv s μ`, i.e. `f` is the Radon-Nikodym derivative of `s` and `μ`. -/
theorem eq_rnDeriv (t : SignedMeasure α) (f : α → ℝ) (hfi : Integrable f μ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure)
(hadd : s = t + μ.withDensityᵥ f) : f =ᵐ[μ] s.rnDeriv μ :=
by
set f' := hfi.1.mk f
have hadd' : s = t + μ.withDensityᵥ f' := by
convert hadd using 2
exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
have := haveLebesgueDecomposition_mk μ hfi.1.measurable_mk htμ hadd'
refine (Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) hfi ?_).symm
rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd, singularPart_add_withDensity_rnDeriv_eq]
