bound_le_one

Mathlib.Probability.Kernel.Defs

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

Lean4

@[simp]
theorem bound_le_one (κ : Kernel α β) [IsZeroOrMarkovKernel κ] : κ.bound ≤ 1 :=
  by
  rcases isEmpty_or_nonempty α
  · simp
  · rcases eq_zero_or_isMarkovKernel κ with rfl | _ <;> simp

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

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

Разделы

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

Аффилиация

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