English
For kernels κ, η and ξ with a fixed decomposition κ = η.withDensity f + ξ, the RN-derivative satisfies that f a = (κ a).rnDeriv (η a) almost everywhere with respect to η a, and κ a and η a are mutually singular on the appropriate part, yielding an almost everywhere equality of RN-deriv to the density.
Русский
Для ядер κ, η и ξ с разложением κ = η.withDensity f + ξ выполняется, что плотность rnDeriv κ η относительно η a равна f a почти всюду по η a, и κ a и η a взаимно сингулярны на соответствующей части, что приводит к почти везде равенству rnDeriv κ η a и плотности f.
LaTeX
$$Eq κ (η.withDensity f + ξ) → Measurable (uncurry f) → ∀ a, (ξ a ⟂ η a) → f a =ᵐ[η a] ∂(κ a)/∂(η a)$$
Lean4
theorem eq_rnDeriv_measure (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (a : α)
(hξ : ξ a ⟂ₘ η a) : f a =ᵐ[η a] ∂(κ a)/∂(η a) :=
by
have : κ a = ξ a + (η a).withDensity (f a) := by rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]
exact (κ a).eq_rnDeriv₀ (hf.comp measurable_prodMk_left).aemeasurable hξ this
