Theorems · Definition · probability

ProbabilityTheory.Kernel.condKernelCDF

{α : Type u_1} →
  {γ : Type u_3} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [MeasurableSpace.CountablyGenerated γ] →
          (κ : ProbabilityTheory.Kernel α (γ × ℝ)) → [ProbabilityTheory.IsFiniteKernel κ] → α × γ → StieltjesFunction ℝ

The conditional kernel CDF of a kernel κ : Kernel α (γ × ℝ), where γ is countably generated.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountablyGeneratedProbabilityTheory.IsFiniteKernel