English
The operator withDensity applied to κ+η with density rnDerivAux equals κ, showing a decomposition of κ into a density over η.
Русский
Оператор withDensity, применённый к κ+η с плотностью rnDerivAux, даёт κ; разложение κ по плотности над η.
LaTeX
$$$$ (κ+η) withDensity (λ a x ↦ Real.toNNReal (rnDerivAux (κ+η) a x)) = κ. $$$$
Lean4
theorem withDensity_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)) = κ :=
by
ext a s hs
rw [Kernel.withDensity_apply']
swap; · fun_prop
simp_rw [ofNNReal_toNNReal]
exact setLIntegral_rnDerivAux κ η a hs