instIsFiniteKernelSingularPart — Mathlib

English

The singularPart of a kernel with respect to itself is zero.

Русский

Сингулярная часть ядра по отношению к самому себе равна нулю.

LaTeX

$$κ.singularPart κ = 0$$

Lean4

instance [hκ : IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (singularPart κ η) :=
  by
  refine ⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩
  have h : withDensity η (rnDeriv κ η) a univ + singularPart κ η a univ = κ a univ :=
    by
    conv_rhs => rw [← rnDeriv_add_singularPart κ η]
    simp
  exact (self_le_add_left _ _).trans (h.le.trans (measure_le_bound _ _ _))

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