Theorems · Inductive type · probability

ProbabilityTheory.IsRatCondKernelCDF

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

a function f : α × β → ℚ → ℝ is called a rational conditional kernel CDF of κ with respect to ν if is measurable, if 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). Also the ℚ → ℝ function f (a, b) should satisfy the properties of a Stieltjes function for (ν a)-almost all b : β.

Defined in

Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Cited by

20 results in Mathlib

Foundations

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