English
For finite kernel κ, any bounded measurable density f, and hf measurable, the RN-derivative of κ.withDensity f with respect to κ equals f a almost everywhere: (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a.
Русский
Для конечного ядра κ и плотности f, измеряемой почти повсюду, выполняется что (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a.
LaTeX
$$$(κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a$$$
Lean4
theorem rnDeriv_withDensity [IsFiniteKernel κ] {f : α → γ → ℝ≥0∞} [IsFiniteKernel (withDensity κ f)]
(hf : Measurable (Function.uncurry f)) (a : α) : (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a :=
by
have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)
have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left
filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2
rw [hx1, κ.withDensity_apply hf, hx2]
