# 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 α β.

• ProbabilityTheory.IsCondKernelCDF: 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 : α × β, 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.
• ProbabilityTheory.IsCondKernelCDF.toKernel: from a function f : α × β → StieltjesFunction with the property hf : IsCondKernelCDF f κ ν, build a kernel (α × β) ℝ such that κ = ν ⊗ₖ hf.toKernel f.
• ProbabilityTheory.IsRatCondKernelCDF: a function f : α × β → ℚ → ℝ is called a rational conditional kernel CDF of κ with respect to ν if is measurable and satisfies the same integral conditions as in the definition of IsCondKernelCDF, and the ℚ → ℝ function f (a, b) satisfies the properties of a Stieltjes function for (ν a)-almost all b : β.

## Main statements #

• ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat: if f : α × β → ℚ → ℝ has the property IsRatCondKernelCDF, then stieltjesOfMeasurableRat f is a function α × β → StieltjesFunction with the property IsCondKernelCDF.
• ProbabilityTheory.compProd_toKernel: for hf : IsCondKernelCDF f κ ν, ν ⊗ₖ hf.toKernel f = κ.
structure ProbabilityTheory.IsRatCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (f : α × β) (κ : ()) (ν : ()) :

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 : β.

• measurable :
• isRatStieltjesPoint_ae : ∀ (a : α), ∀ᵐ (b : β) ∂ν a,
• integrable : ∀ (a : α) (q : ), MeasureTheory.Integrable (fun (b : β) => f (a, b) q) (ν a)
• setIntegral : ∀ (a : α) {s : Set β}, ∀ (q : ), ∫ (b : β) in s, f (a, b) qν a = ((κ a) (s ×ˢ Set.Iic q)).toReal
Instances For
theorem ProbabilityTheory.IsRatCondKernelCDF.measurable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) :
theorem ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) :
∀ᵐ (b : β) ∂ν a,
theorem ProbabilityTheory.IsRatCondKernelCDF.integrable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) (q : ) :
MeasureTheory.Integrable (fun (b : β) => f (a, b) q) (ν a)
theorem ProbabilityTheory.IsRatCondKernelCDF.setIntegral {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) {s : Set β} (_hs : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (b : β) ∂ν a, Monotone (f (a, b))
theorem ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (b : β) ∂ν a, ∀ (q : ), ⨅ (r : ()), f (a, b) r = f (a, b) q
theorem ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) :
(fun (b : β) => () q) =ᵐ[ν a] fun (b : β) => f (a, b) q
theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) {s : Set β} (hs : ) :
∫ (b : β) in s, () 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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) {s : Set β} (hs : ) :
∫ (b : β) in s, () 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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) {s : Set β} (hs : ) :
∫⁻ (b : β) in s, ENNReal.ofReal (() q)ν a = (κ a) (s ×ˢ Set.Iic q)
theorem ProbabilityTheory.set_lintegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (x : ) {s : Set β} (hs : ) :
∫⁻ (b : β) in s, ENNReal.ofReal (() x)ν a = (κ a) (s ×ˢ )
theorem ProbabilityTheory.lintegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (x : ) :
∫⁻ (b : β), ENNReal.ofReal (() x)ν a = (κ a) (Set.univ ×ˢ )
theorem ProbabilityTheory.integrable_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (x : ) :
MeasureTheory.Integrable (fun (b : β) => () x) (ν a)
theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (x : ) {s : Set β} (hs : ) :
∫ (b : β) in s, () xν a = ((κ a) (s ×ˢ )).toReal
@[deprecated ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat]
theorem ProbabilityTheory.set_integral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (x : ) {s : Set β} (hs : ) :
∫ (b : β) in s, () xν a = ((κ a) (s ×ˢ )).toReal

Alias of ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat.

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

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 :
• 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 β}, ∀ (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α : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) :
theorem ProbabilityTheory.IsRatCondKernelCDFAux.mono' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (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α : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) (q : ) :
∀ᵐ (c : β) ∂ν a, 0 f (a, c) q
theorem ProbabilityTheory.IsRatCondKernelCDFAux.le_one' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) (q : ) :
∀ᵐ (c : β) ∂ν a, f (a, c) q 1
theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (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α : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (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α : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) (q : ) :
MeasureTheory.Integrable (fun (c : β) => f (a, c) q) (ν a)
theorem ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × β} {κ : ()} {ν : ()} (self : ) (a : α) {A : Set β} (_hA : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) :
Measurable fun (t : β) => f (a, t) q
theorem ProbabilityTheory.IsRatCondKernelCDFAux.mono {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))
theorem ProbabilityTheory.IsRatCondKernelCDFAux.nonneg {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (c : β) ∂ν a, ∀ (q : ), 0 f (a, c) q
theorem ProbabilityTheory.IsRatCondKernelCDFAux.le_one {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (c : β) ∂ν a, ∀ (q : ), f (a, c) q 1
theorem ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atBot (nhds 0)
theorem ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (t : β) ∂ν a, ∀ (q : ), BddBelow (Set.range fun (r : ()) => f (a, t) r)
theorem ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) :
MeasureTheory.Integrable (fun (t : β) => ⨅ (r : ()), f (a, t) r) (ν a)
theorem MeasureTheory.Measure.iInf_rat_gt_prod_Iic {α : Type u_1} {mα : } {ρ : } {s : Set α} (hs : ) (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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) {A : Set β} (hA : ) :
∫ (t : β) in A, ⨅ (r : ()), 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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) (q : ) {A : Set β} (hA : ) :
∫ (t : β) in A, ⨅ (r : ()), 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α : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (t : β) ∂ν a, ∀ (q : ), ⨅ (r : ()), f (a, t) r = f (a, t) q
theorem ProbabilityTheory.IsRatCondKernelCDFAux.isRatStieltjesPoint_ae {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) (a : α) :
∀ᵐ (t : β) ∂ν a,
theorem ProbabilityTheory.IsRatCondKernelCDFAux.isRatCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) :
structure ProbabilityTheory.IsCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (f : α × βStieltjesFunction) (κ : ()) (ν : ()) :

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.

• measurable : ∀ (x : ), Measurable fun (p : α × β) => (f p) x
• integrable : ∀ (a : α) (x : ), MeasureTheory.Integrable (fun (b : β) => (f (a, b)) x) (ν a)
• tendsto_atTop_one : ∀ (p : α × β), Filter.Tendsto ((f p)) Filter.atTop (nhds 1)
• tendsto_atBot_zero : ∀ (p : α × β), Filter.Tendsto ((f p)) Filter.atBot (nhds 0)
• setIntegral : ∀ (a : α) {s : Set β}, ∀ (x : ), ∫ (b : β) in s, (f (a, b)) xν a = ((κ a) (s ×ˢ )).toReal
Instances For
theorem ProbabilityTheory.IsCondKernelCDF.measurable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} (self : ) (x : ) :
Measurable fun (p : α × β) => (f p) x
theorem ProbabilityTheory.IsCondKernelCDF.integrable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} (self : ) (a : α) (x : ) :
MeasureTheory.Integrable (fun (b : β) => (f (a, b)) x) (ν a)
theorem ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} (self : ) (p : α × β) :
Filter.Tendsto ((f p)) Filter.atTop (nhds 1)
theorem ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} (self : ) (p : α × β) :
Filter.Tendsto ((f p)) Filter.atBot (nhds 0)
theorem ProbabilityTheory.IsCondKernelCDF.setIntegral {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} (self : ) (a : α) {s : Set β} (_hs : ) (x : ) :
∫ (b : β) in s, (f (a, b)) xν a = ((κ a) (s ×ˢ )).toReal
theorem ProbabilityTheory.IsCondKernelCDF.nonneg {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (p : α × β) (x : ) :
0 (f p) x
theorem ProbabilityTheory.IsCondKernelCDF.le_one {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (p : α × β) (x : ) :
(f p) x 1
theorem ProbabilityTheory.IsCondKernelCDF.integral {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) (x : ) :
∫ (b : β), (f (a, b)) xν a = ((κ a) (Set.univ ×ˢ )).toReal
theorem ProbabilityTheory.IsCondKernelCDF.set_lintegral {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) {s : Set β} (hs : ) (x : ) :
∫⁻ (b : β) in s, ENNReal.ofReal ((f (a, b)) x)ν a = (κ a) (s ×ˢ )
theorem ProbabilityTheory.IsCondKernelCDF.lintegral {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) (x : ) :
∫⁻ (b : β), ENNReal.ofReal ((f (a, b)) x)ν a = (κ a) (Set.univ ×ˢ )
theorem ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × β} (hf : ) :
theorem ProbabilityTheory.StieltjesFunction.measurable_measure {α : Type u_1} {mα : } {f : } (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α : } :
{x : } → {κ : ()} → {ν : ()} → (f : α × βStieltjesFunction) → ()

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
• = fun (p : α × β) => (f p).measure,
Instances For
theorem ProbabilityTheory.IsCondKernelCDF.toKernel_apply {α : Type u_1} {β : Type u_2} {mα : } :
∀ {x : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} {hf : } (p : α × β), = (f p).measure
instance ProbabilityTheory.instIsMarkovKernel_toKernel {α : Type u_1} {β : Type u_2} {mα : } :
∀ {x : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} {hf : },
Equations
• =
theorem ProbabilityTheory.IsCondKernelCDF.toKernel_Iic {α : Type u_1} {β : Type u_2} {mα : } :
∀ {x : } {f : α × βStieltjesFunction} {κ : ()} {ν : ()} {hf : } (p : α × β) (x_1 : ), () (Set.Iic x_1) = ENNReal.ofReal ((f p) x_1)
theorem ProbabilityTheory.set_lintegral_toKernel_Iic {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) (x : ) {s : Set β} (hs : ) :
∫⁻ (b : β) in s, ( (a, b)) ()ν a = (κ a) (s ×ˢ )
theorem ProbabilityTheory.set_lintegral_toKernel_univ {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) {s : Set β} (hs : ) :
∫⁻ (b : β) in s, ( (a, b)) Set.univν a = (κ a) (s ×ˢ Set.univ)
theorem ProbabilityTheory.lintegral_toKernel_univ {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) :
∫⁻ (b : β), ( (a, b)) Set.univν a = (κ a) Set.univ
theorem ProbabilityTheory.set_lintegral_toKernel_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) {s : Set β} (hs : ) {t : } (ht : ) :
∫⁻ (b : β) in s, ( (a, b)) tν a = (κ a) (s ×ˢ t)
theorem ProbabilityTheory.lintegral_toKernel_mem {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) (a : α) {s : Set (β × )} (hs : ) :
∫⁻ (b : β), ( (a, b)) {y : | (b, y) s}ν a = (κ a) s
theorem ProbabilityTheory.compProd_toKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {ν : ()} {f : α × βStieltjesFunction} (hf : ) :