Documentation

Mathlib.Probability.Kernel.Disintegration.CdfToKernel

Building a Markov kernel from a conditional cumulative distribution function #

Let κ : kernel α (β × ℝ) and ν : kernel α β be two finite kernels. A function f : α × β → StieltjesFunction is called a conditional kernel CDF of κ with respect to ν if it is measurable, tends to 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 (s ×ˢ Iic x)).toReal.

From such a function with property hf : IsCondKernelCDF f κ ν, we can build a kernel (α × β) ℝ denoted by hf.toKernel f such that κ = ν ⊗ₖ hf.toKernel f.

Main definitions #

Let κ : kernel α (β × ℝ) and ν : kernel α β.

Main statements #

structure ProbabilityTheory.IsRatCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β) (κ : (ProbabilityTheory.kernel α (β × ))) (ν : (ProbabilityTheory.kernel α β)) :

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 (s ×ˢ Iic x)).toReal. Also the ℚ → ℝ function f (a, b) should satisfy the properties of a Sieltjes function for (ν a)-almost all b : β.

Instances For
    theorem ProbabilityTheory.IsRatCondKernelCDF.measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDF f κ ν) :
    theorem ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ (b : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, b)
    theorem ProbabilityTheory.IsRatCondKernelCDF.integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ) :
    MeasureTheory.Integrable (fun (b : β) => f (a, b) q) (ν a)
    theorem ProbabilityTheory.IsRatCondKernelCDF.setIntegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) {s : Set β} (_hs : MeasurableSet s) (q : ) :
    ∫ (b : β) in s, f (a, b) qν a = ((κ a) (s ×ˢ Set.Iic q)).toReal
    theorem ProbabilityTheory.IsRatCondKernelCDF.mono {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ (b : β) ∂ν a, Monotone (f (a, b))
    theorem ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ (b : β) ∂ν a, Filter.Tendsto (f (a, b)) Filter.atTop (nhds 1)
    theorem ProbabilityTheory.IsRatCondKernelCDF.tendsto_atBot_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ (b : β) ∂ν a, Filter.Tendsto (f (a, b)) Filter.atBot (nhds 0)
    theorem ProbabilityTheory.IsRatCondKernelCDF.iInf_rat_gt_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ (b : β) ∂ν a, ∀ (q : ), ⨅ (r : (Set.Ioi q)), f (a, b) r = f (a, b) q
    theorem ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ) :
    (fun (b : β) => (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) q) =ᵐ[ν a] fun (b : β) => f (a, b) q
    theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ) {s : Set β} (hs : MeasurableSet s) :
    ∫ (b : β) in s, (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) qν a = ((κ a) (s ×ˢ Set.Iic q)).toReal
    @[deprecated ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat]
    theorem ProbabilityTheory.set_integral_stieltjesOfMeasurableRat_rat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ) {s : Set β} (hs : MeasurableSet s) :
    ∫ (b : β) in s, (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) qν a = ((κ a) (s ×ˢ Set.Iic q)).toReal

    Alias of ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat.

    theorem ProbabilityTheory.set_lintegral_stieltjesOfMeasurableRat_rat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ) {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ (b : β) in s, ENNReal.ofReal ((ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) q)ν a = (κ a) (s ×ˢ Set.Iic q)
    theorem ProbabilityTheory.set_lintegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ) {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ (b : β) in s, ENNReal.ofReal ((ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) x)ν a = (κ a) (s ×ˢ Set.Iic x)
    theorem ProbabilityTheory.lintegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ) :
    ∫⁻ (b : β), ENNReal.ofReal ((ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) x)ν a = (κ a) (Set.univ ×ˢ Set.Iic x)
    theorem ProbabilityTheory.integrable_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ) :
    MeasureTheory.Integrable (fun (b : β) => (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) x) (ν a)
    theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ) {s : Set β} (hs : MeasurableSet s) :
    ∫ (b : β) in s, (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) xν a = ((κ a) (s ×ˢ Set.Iic x)).toReal
    @[deprecated ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat]
    theorem ProbabilityTheory.set_integral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ) {s : Set β} (hs : MeasurableSet s) :
    ∫ (b : β) in s, (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) xν a = ((κ a) (s ×ˢ Set.Iic x)).toReal

    Alias of ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat.

    theorem ProbabilityTheory.integral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ) :
    ∫ (b : β), (ProbabilityTheory.stieltjesOfMeasurableRat f (a, b)) xν a = ((κ a) (Set.univ ×ˢ Set.Iic x)).toReal
    structure ProbabilityTheory.IsRatCondKernelCDFAux {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β) (κ : (ProbabilityTheory.kernel α (β × ))) (ν : (ProbabilityTheory.kernel α β)) :

    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.

    • measurable : Measurable f
    • mono' : ∀ (a : α) {q r : }, q r∀ᵐ (c : β) ∂ν a, f (a, c) q f (a, c) r
    • nonneg' : ∀ (a : α) (q : ), ∀ᵐ (c : β) ∂ν a, 0 f (a, c) q
    • le_one' : ∀ (a : α) (q : ), ∀ᵐ (c : β) ∂ν a, f (a, c) q 1
    • tendsto_integral_of_antitone : ∀ (a : α) (seq : ), Antitone seqFilter.Tendsto seq Filter.atTop Filter.atBotFilter.Tendsto (fun (m : ) => ∫ (c : β), f (a, c) (seq m)ν a) Filter.atTop (nhds 0)
    • tendsto_integral_of_monotone : ∀ (a : α) (seq : ), Monotone seqFilter.Tendsto seq Filter.atTop Filter.atTopFilter.Tendsto (fun (m : ) => ∫ (c : β), f (a, c) (seq m)ν a) Filter.atTop (nhds ((ν a) Set.univ).toReal)
    • integrable : ∀ (a : α) (q : ), MeasureTheory.Integrable (fun (c : β) => f (a, c) q) (ν a)
    • setIntegral : ∀ (a : α) {A : Set β}, MeasurableSet A∀ (q : ), ∫ (c : β) in A, f (a, c) qν a = ((κ a) (A ×ˢ Set.Iic q)).toReal
    Instances For
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) :
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.mono' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) {q : } {r : } (_hqr : q r) :
      ∀ᵐ (c : β) ∂ν a, f (a, c) q f (a, c) r
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.nonneg' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) (q : ) :
      ∀ᵐ (c : β) ∂ν a, 0 f (a, c) q
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.le_one' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) (q : ) :
      ∀ᵐ (c : β) ∂ν a, f (a, c) q 1
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) (seq : ) (_hs : Antitone seq) (_hs_tendsto : Filter.Tendsto seq Filter.atTop Filter.atBot) :
      Filter.Tendsto (fun (m : ) => ∫ (c : β), f (a, c) (seq m)ν a) Filter.atTop (nhds 0)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) (seq : ) (_hs : Monotone seq) (_hs_tendsto : Filter.Tendsto seq Filter.atTop Filter.atTop) :
      Filter.Tendsto (fun (m : ) => ∫ (c : β), f (a, c) (seq m)ν a) Filter.atTop (nhds ((ν a) Set.univ).toReal)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) (q : ) :
      MeasureTheory.Integrable (fun (c : β) => f (a, c) q) (ν a)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) {A : Set β} (_hA : MeasurableSet A) (q : ) :
      ∫ (c : β) in A, f (a, c) qν a = ((κ a) (A ×ˢ Set.Iic q)).toReal
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.measurable_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) (q : ) :
      Measurable fun (t : β) => f (a, t) q
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.mono {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) :
      ∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.nonneg {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) :
      ∀ᵐ (c : β) ∂ν a, ∀ (q : ), 0 f (a, c) q
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.le_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) :
      ∀ᵐ (c : β) ∂ν a, ∀ (q : ), f (a, c) q 1
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ) (hseq : Antitone seq) (hseq_tendsto : Filter.Tendsto seq Filter.atTop Filter.atBot) :
      ∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun (m : ) => f (a, c) (seq m)) Filter.atTop (nhds 0)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_one_of_monotone {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ) (hseq : Monotone seq) (hseq_tendsto : Filter.Tendsto seq Filter.atTop Filter.atTop) :
      ∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun (m : ) => f (a, c) (seq m)) Filter.atTop (nhds 1)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) :
      ∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atTop (nhds 1)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) :
      ∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atBot (nhds 0)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) (a : α) :
      ∀ᵐ (t : β) ∂ν a, ∀ (q : ), BddBelow (Set.range fun (r : (Set.Ioi q)) => f (a, t) r)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (q : ) :
      MeasureTheory.Integrable (fun (t : β) => ⨅ (r : (Set.Ioi q)), f (a, t) r) (ν a)
      theorem MeasureTheory.Measure.iInf_rat_gt_prod_Iic {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × )} [MeasureTheory.IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) (t : ) :
      ⨅ (r : { r' : // t < r' }), ρ (s ×ˢ Set.Iic r) = ρ (s ×ˢ Set.Iic t)
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] (a : α) (q : ) {A : Set β} (hA : MeasurableSet A) :
      ∫ (t : β) in A, ⨅ (r : (Set.Ioi q)), f (a, t) rν a = ((κ a) (A ×ˢ Set.Iic q)).toReal
      @[deprecated ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt]
      theorem ProbabilityTheory.IsRatCondKernelCDFAux.set_integral_iInf_rat_gt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] (a : α) (q : ) {A : Set β} (hA : MeasurableSet A) :
      ∫ (t : β) in A, ⨅ (r : (Set.Ioi q)), f (a, t) rν a = ((κ a) (A ×ˢ Set.Iic q)).toReal

      Alias of ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt.

      theorem ProbabilityTheory.IsRatCondKernelCDFAux.iInf_rat_gt_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × β} (hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] (a : α) :
      ∀ᵐ (t : β) ∂ν a, ∀ (q : ), ⨅ (r : (Set.Ioi q)), f (a, t) r = f (a, t) q
      structure ProbabilityTheory.IsCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × βStieltjesFunction) (κ : (ProbabilityTheory.kernel α (β × ))) (ν : (ProbabilityTheory.kernel α β)) :

      A function f : α × β → StieltjesFunction is called a conditional kernel CDF of κ with respect to ν if it is measurable, tends to 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 (s ×ˢ Iic x)).toReal.

      Instances For
        theorem ProbabilityTheory.IsCondKernelCDF.measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsCondKernelCDF f κ ν) (x : ) :
        Measurable fun (p : α × β) => (f p) x
        theorem ProbabilityTheory.IsCondKernelCDF.integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) (x : ) :
        MeasureTheory.Integrable (fun (b : β) => (f (a, b)) x) (ν a)
        theorem ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsCondKernelCDF f κ ν) (p : α × β) :
        Filter.Tendsto ((f p)) Filter.atTop (nhds 1)
        theorem ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsCondKernelCDF f κ ν) (p : α × β) :
        Filter.Tendsto ((f p)) Filter.atBot (nhds 0)
        theorem ProbabilityTheory.IsCondKernelCDF.setIntegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} (self : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set β} (_hs : MeasurableSet s) (x : ) :
        ∫ (b : β) in s, (f (a, b)) xν a = ((κ a) (s ×ˢ Set.Iic x)).toReal
        theorem ProbabilityTheory.IsCondKernelCDF.nonneg {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (p : α × β) (x : ) :
        0 (f p) x
        theorem ProbabilityTheory.IsCondKernelCDF.le_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (p : α × β) (x : ) :
        (f p) x 1
        theorem ProbabilityTheory.IsCondKernelCDF.integral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) (x : ) :
        ∫ (b : β), (f (a, b)) xν a = ((κ a) (Set.univ ×ˢ Set.Iic x)).toReal
        theorem ProbabilityTheory.IsCondKernelCDF.set_lintegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsFiniteKernel κ] {f : α × βStieltjesFunction} (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set β} (hs : MeasurableSet s) (x : ) :
        ∫⁻ (b : β) in s, ENNReal.ofReal ((f (a, b)) x)ν a = (κ a) (s ×ˢ Set.Iic x)
        theorem ProbabilityTheory.IsCondKernelCDF.lintegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsFiniteKernel κ] {f : α × βStieltjesFunction} (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) (x : ) :
        ∫⁻ (b : β), ENNReal.ofReal ((f (a, b)) x)ν a = (κ a) (Set.univ ×ˢ Set.Iic x)
        theorem ProbabilityTheory.StieltjesFunction.measurable_measure {α : Type u_1} {mα : MeasurableSpace α} {f : αStieltjesFunction} (hf : ∀ (q : ), Measurable fun (a : α) => (f a) q) (hf_bot : ∀ (a : α), Filter.Tendsto ((f a)) Filter.atBot (nhds 0)) (hf_top : ∀ (a : α), Filter.Tendsto ((f a)) Filter.atTop (nhds 1)) :
        Measurable fun (a : α) => (f a).measure

        A measurable function α → StieltjesFunction with limits 0 at -∞ and 1 at +∞ gives a measurable function α → Measure ℝ by taking StieltjesFunction.measure at each point.

        noncomputable def ProbabilityTheory.IsCondKernelCDF.toKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} :
        {x : MeasurableSpace β} → {κ : (ProbabilityTheory.kernel α (β × ))} → {ν : (ProbabilityTheory.kernel α β)} → (f : α × βStieltjesFunction) → ProbabilityTheory.IsCondKernelCDF f κ ν(ProbabilityTheory.kernel (α × β) )

        A function f : α × β → StieltjesFunction with the property IsCondKernelCDF f κ ν gives a Markov kernel from α × β to , by taking for each p : α × β the measure defined by f p.

        Equations
        Instances For
          theorem ProbabilityTheory.IsCondKernelCDF.toKernel_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} :
          ∀ {x : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {hf : ProbabilityTheory.IsCondKernelCDF f κ ν} (p : α × β), (ProbabilityTheory.IsCondKernelCDF.toKernel f hf) p = (f p).measure
          theorem ProbabilityTheory.IsCondKernelCDF.toKernel_Iic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} :
          ∀ {x : MeasurableSpace β} {f : α × βStieltjesFunction} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {hf : ProbabilityTheory.IsCondKernelCDF f κ ν} (p : α × β) (x_1 : ), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) p) (Set.Iic x_1) = ENNReal.ofReal ((f p) x_1)
          theorem ProbabilityTheory.set_lintegral_toKernel_Iic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) (x : ) {s : Set β} (hs : MeasurableSet s) :
          ∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) (Set.Iic x)ν a = (κ a) (s ×ˢ Set.Iic x)
          theorem ProbabilityTheory.set_lintegral_toKernel_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set β} (hs : MeasurableSet s) :
          ∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) Set.univν a = (κ a) (s ×ˢ Set.univ)
          theorem ProbabilityTheory.lintegral_toKernel_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) :
          ∫⁻ (b : β), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) Set.univν a = (κ a) Set.univ
          theorem ProbabilityTheory.set_lintegral_toKernel_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set } (ht : MeasurableSet t) :
          ∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) tν a = (κ a) (s ×ˢ t)
          theorem ProbabilityTheory.lintegral_toKernel_mem {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : (ProbabilityTheory.kernel α (β × ))} {ν : (ProbabilityTheory.kernel α β)} {f : α × βStieltjesFunction} [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set (β × )} (hs : MeasurableSet s) :
          ∫⁻ (b : β), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) {y : | (b, y) s}ν a = (κ a) s