withDensity_rnDerivAux — Mathlib

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

Похожие утверждения