bound

Mathlib.Probability.Kernel.Defs

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

Lean4

/-- A constant `C : ℝ≥0∞` such that `C < ∞` for a finite kernel
(`ProbabilityTheory.IsFiniteKernel.bound_lt_top κ`) and for all `a : α` and `s : Set β`,
`κ a s ≤ C` (`ProbabilityTheory.Kernel.measure_le_bound κ a s`). -/
noncomputable def bound (κ : Kernel α β) : ℝ≥0∞ :=
  ⨆ a, κ a Set.univ

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

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

Разделы

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

Аффилиация

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