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 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).

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 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).real (s ×ˢ Iic x).
• 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α : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β → ℚ → ℝ) (κ : Kernel α (β × ℝ)) (ν : 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 Sieltjes function for (ν a)-almost all b : β.

• measurable : Measurable f
• isRatStieltjesPoint_ae (a : α) : ∀ᵐ (b : β) ∂ν a, IsRatStieltjesPoint f (a, b)
• integrable (a : α) (q : ℚ) : MeasureTheory.Integrable (fun (b : β) => f (a, b) q) (ν a)
• setIntegral (a : α) {s : Set β} (_hs : MeasurableSet s) (q : ℚ) : ∫ (b : β) in s, f (a, b) q ∂ν a = (κ a).real (s ×ˢ Set.Iic ↑q)

theorem ProbabilityTheory.IsRatCondKernelCDF.mono {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) : (fun (b : β) => ↑(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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) {s : Set β} (hs : MeasurableSet s) : ∫ (b : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q ∂ν a = (κ a).real (s ×ˢ Set.Iic ↑q)

theorem ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ∂ν a = (κ a) (s ×ˢ Set.Iic ↑q)

theorem ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) : ∫⁻ (b : β), ENNReal.ofReal (↑(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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) : MeasureTheory.Integrable (fun (b : β) => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)

theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β} (hs : MeasurableSet s) : ∫ (b : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = (κ a).real (s ×ˢ Set.Iic x)

theorem ProbabilityTheory.integral_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) : ∫ (b : β), ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = (κ a).real (Set.univ ×ˢ Set.Iic x)

structure ProbabilityTheory.IsRatCondKernelCDFAux {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β → ℚ → ℝ) (κ : Kernel α (β × ℝ)) (ν : 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.

• measurable : Measurable f
• mono' (a : α) {q r : ℚ} (_hqr : 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 : ℕ → ℚ) (_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)
• tendsto_integral_of_monotone (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).real Set.univ))
• integrable (a : α) (q : ℚ) : MeasureTheory.Integrable (fun (c : β) => f (a, c) q) (ν a)
• setIntegral (a : α) {A : Set β} (_hA : MeasurableSet A) (q : ℚ) : ∫ (c : β) in A, f (a, c) q ∂ν a = (κ a).real (A ×ˢ Set.Iic ↑q)

theorem ProbabilityTheory.IsRatCondKernelCDFAux.measurable_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) (a : α) : ∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))

theorem ProbabilityTheory.IsRatCondKernelCDFAux.nonneg {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [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 α} {ρ : Measure (α × ℝ)} [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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) (q : ℚ) {A : Set β} (hA : MeasurableSet A) : ∫ (t : β) in A, ⨅ (r : ↑(Set.Ioi q)), f (a, t) ↑r ∂ν a = (κ a).real (A ×ˢ Set.Iic ↑q)

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

theorem ProbabilityTheory.IsRatCondKernelCDFAux.isRatStieltjesPoint_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) : ∀ᵐ (t : β) ∂ν a, IsRatStieltjesPoint f (a, t)

theorem ProbabilityTheory.IsRatCondKernelCDFAux.isRatCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel κ] [IsFiniteKernel ν] : IsRatCondKernelCDF f κ ν

structure ProbabilityTheory.IsCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β → StieltjesFunction) (κ : Kernel α (β × ℝ)) (ν : 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).

• 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 β} (_hs : MeasurableSet s) (x : ℝ) : ∫ (b : β) in s, ↑(f (a, b)) x ∂ν a = (κ a).real (s ×ˢ Set.Iic x)

theorem ProbabilityTheory.IsCondKernelCDF.nonneg {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (p : α × β) (x : ℝ) : 0 ≤ ↑(f p) x

theorem ProbabilityTheory.IsCondKernelCDF.le_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (p : α × β) (x : ℝ) : ↑(f p) x ≤ 1

theorem ProbabilityTheory.IsCondKernelCDF.integral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) : ∫ (b : β), ↑(f (a, b)) x ∂ν a = (κ a).real (Set.univ ×ˢ Set.Iic x)

theorem ProbabilityTheory.IsCondKernelCDF.setLIntegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} [IsFiniteKernel κ] {f : α × β → StieltjesFunction} (hf : 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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} [IsFiniteKernel κ] {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) : ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (Set.univ ×ˢ Set.Iic x)

theorem ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDF f κ ν) [IsFiniteKernel κ] : IsCondKernelCDF (stieltjesOfMeasurableRat f ⋯) κ ν

noncomputable def ProbabilityTheory.IsCondKernelCDF.toKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x✝ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} (f : α × β → StieltjesFunction) (hf : IsCondKernelCDF f κ ν) : 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

• ProbabilityTheory.IsCondKernelCDF.toKernel f hf = { toFun := fun (p : α × β) => (f p).measure, measurable' := ⋯ }

theorem ProbabilityTheory.IsCondKernelCDF.toKernel_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x✝ : MeasurableSpace β} {f : α × β → StieltjesFunction} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {hf : IsCondKernelCDF f κ ν} (p : α × β) : (toKernel f hf) p = (f p).measure

instance ProbabilityTheory.instIsMarkovKernel_toKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x✝ : MeasurableSpace β} {f : α × β → StieltjesFunction} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {hf : IsCondKernelCDF f κ ν} : IsMarkovKernel (IsCondKernelCDF.toKernel f hf)

theorem ProbabilityTheory.IsCondKernelCDF.toKernel_Iic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x✝ : MeasurableSpace β} {f : α × β → StieltjesFunction} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {hf : IsCondKernelCDF f κ ν} (p : α × β) (x : ℝ) : ((toKernel f hf) p) (Set.Iic x) = ENNReal.ofReal (↑(f p) x)

theorem ProbabilityTheory.setLIntegral_toKernel_Iic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Set.Iic x) ∂ν a = (κ a) (s ×ˢ Set.Iic x)

theorem ProbabilityTheory.setLIntegral_toKernel_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) {s : Set β} (hs : MeasurableSet s) : ∫⁻ (b : β) in s, ((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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) Set.univ ∂ν a = (κ a) Set.univ

theorem ProbabilityTheory.setLIntegral_toKernel_prod {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set ℝ} (ht : MeasurableSet t) : ∫⁻ (b : β) in s, ((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 β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) {s : Set (β × ℝ)} (hs : MeasurableSet s) : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' s) ∂ν a = (κ a) s

theorem ProbabilityTheory.compProd_toKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α (β × ℝ)} {ν : Kernel α β} {f : α × β → StieltjesFunction} [IsFiniteKernel κ] [IsSFiniteKernel ν] (hf : IsCondKernelCDF f κ ν) : ν.compProd (IsCondKernelCDF.toKernel f hf) = κ