rnDeriv_singularPart — Mathlib

English

The RN-derivative of κ with respect to η equals zero almost everywhere with respect to η a on the singular part, i.e., rnDeriv (singularPart κ ν) ν a = 0 a.e. w.r.t. ν a.

Русский

Плотность rnDeriv ядра κ по η сужается к нулю почти всюду на сингулярной части, т.е. rnDeriv (singularPart κ ν) ν a = 0 почти всюду по ν a.

LaTeX

$$rnDeriv (singularPart κ ν) ν a = 0 (a.e. w.r.t. ν a)$$

Lean4

theorem rnDeriv_singularPart (κ ν : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) :
    rnDeriv (singularPart κ ν) ν a =ᵐ[ν a] 0 :=
  by
  filter_upwards [(singularPart κ ν).rnDeriv_eq_rnDeriv_measure,
    (Measure.rnDeriv_eq_zero _ _).mpr (mutuallySingular_singularPart κ ν a)] with x h1 h2
  rw [h1, h2]

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