integrable — Mathlib

English

If κ is a Markov kernel, then for finite μ, the real-valued kernel κ x restricted to s is integrable with respect to μ for any measurable s.

Русский

Если κ — марковское ядро, то для конечной меры μ интегрируемо по x функция x ↦ (κ x).real s.

LaTeX

$$$\\mathrm{Integrable}\\, (a \\mapsto (κ a).real s) \\; \\text{ w.r.t. } μ$$$

Lean4

theorem integrable (μ : Measure α) [IsFiniteMeasure μ] (κ : Kernel α β) [IsMarkovKernel κ] {s : Set β}
    (hs : MeasurableSet s) : Integrable (fun x => (κ x).real s) μ :=
  IsFiniteKernel.integrable μ κ hs

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