Theorems · Inductive type · probability

ProbabilityTheory.IsRatCondKernelCDFAux

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (α × β → ℚ → ℝ) → ProbabilityTheory.Kernel α (β × ℝ) → ProbabilityTheory.Kernel α β → Prop

This property implies IsRatCondKernelCDF. The measurability, integrability and integral conditions are the same, but the limit properties of IsRatCondKernelCDF are replaced by limits of integrals.

Defined in

Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Cited by

24 results in Mathlib

Foundations

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