Theorems · Definition · probability

ProbabilityTheory.Kernel.seq

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (κ : ProbabilityTheory.Kernel α β) →
          [h : ProbabilityTheory.IsSFiniteKernel κ] → ℕ → ProbabilityTheory.Kernel α β

A sequence of finite kernels such that κ = ProbabilityTheory.Kernel.sum (seq κ). See ProbabilityTheory.Kernel.isFiniteKernel_seq and ProbabilityTheory.Kernel.kernel_sum_seq.

Defined in

Mathlib.Probability.Kernel.Defs

Cited by

12 results in Mathlib

Foundations

Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ProbabilityTheory.IsSFiniteKernel