withDensity_one

Mathlib.Probability.Kernel.WithDensity

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

← MathLib Explorer

English

If f ≡ 1, then κ.withDensity f = κ.

Русский

Если плотность равна единице, то withDensity κ 1 = κ.

LaTeX

$$Kernel.withDensity κ 1 = κ$$

Lean4

@[simp]
theorem withDensity_one (κ : Kernel α β) [IsSFiniteKernel κ] : Kernel.withDensity κ 1 = κ := by ext;
  rw [Kernel.withDensity_apply _ measurable_const]; simp

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

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

Разделы

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

Аффилиация

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