Theorems · Inductive type · probability

ProbabilityTheory.IsSFiniteKernel

{α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop

A kernel is s-finite if it can be written as the sum of countably many finite kernels.

Defined in

Mathlib.Probability.Kernel.Defs

Cited by

248 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms