singularPart_self

Mathlib.Probability.Kernel.RadonNikodym

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.singularPart_self

← MathLib Explorer

English

For a kernel κ, the singular part of κ with respect to itself is zero; i.e., κ.singularPart κ = 0.

Русский

Для ядра κ сингулярная часть относительно самoй κ равна нулю.

LaTeX

$$κ.singularPart κ = 0$$

Lean4

@[simp]
theorem singularPart_self (κ : Kernel α γ) [IsFiniteKernel κ] : κ.singularPart κ = 0 := by ext : 1;
  rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru