measurable_rnDeriv — Mathlib

English

The kernel κ equals the sum of its absolutely continuous part with respect to η and its singular part with respect to η.

Русский

Ядро κ равно сумме своей абсолютоно непрерывной части по отношению к η и своей сингулярной части по отношению к η.

LaTeX

$$$\text{withDensity}(\eta)(\mathrm{rnDeriv}(\kappa, \eta)) + \mathrm{singularPart}(\kappa, \eta) = \kappa$$$

Lean4

@[fun_prop]
theorem measurable_rnDeriv (κ η : Kernel α γ) : Measurable (fun p : α × γ ↦ rnDeriv κ η p.1 p.2) :=
  by
  simp_rw [rnDeriv_def]
  exact (measurable_rnDerivAux κ _).ennreal_ofReal.div (measurable_const.sub (measurable_rnDerivAux κ _)).ennreal_ofReal

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