Theorems · Inductive type · probability

ProbabilityTheory.IsCondKernelCDF

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

A function f : α × β → StieltjesFunction ℝ is called a conditional kernel CDF of κ with respect to ν if it is measurable, tends to 0 at -∞ and to 1 at +∞ for all p : α × β, fun b ↦ f (a, b) x is (ν a)-integrable for all a : α and x : ℝ and for all measurable sets s : Set β, ∫ b in s, f (a, b) x ∂(ν a) = (κ a).real (s ×ˢ Iic x).

Defined in

Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Cited by

22 results in Mathlib

Foundations

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