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α : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β → ℚ → ℝ) (κ : ↥(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 (s ×ˢ Iic x)).toReal. 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, ProbabilityTheory.IsRatStieltjesPoint f (a, b)
• integrable : ∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun (b : β) => f (a, b) q) (ν a)
• setIntegral : ∀ (a : α) {s : Set β}, 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) =ᶠ[MeasureTheory.Measure.ae (ν 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 α β)) : 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 : ℚ}, 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 seq → 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 : ℕ → ℚ), Monotone seq → 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)
• 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

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

theorem ProbabilityTheory.IsRatCondKernelCDFAux.isRatStieltjesPoint_ae {α : 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, ProbabilityTheory.IsRatStieltjesPoint f (a, t)

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

structure ProbabilityTheory.IsCondKernelCDF {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α × β → 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 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 β}, 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.isCondKernelCDF_stieltjesOfMeasurableRat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ↥(ProbabilityTheory.kernel α (β × ℝ))} {ν : ↥(ProbabilityTheory.kernel α β)} {f : α × β → ℚ → ℝ} (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsCondKernelCDF (ProbabilityTheory.stieltjesOfMeasurableRat f ⋯) κ ν

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 : α) => StieltjesFunction.measure (f a)

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

• ProbabilityTheory.IsCondKernelCDF.toKernel f hf = { val := fun (p : α × β) => StieltjesFunction.measure (f p), property := ⋯ }

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 = StieltjesFunction.measure (f p)

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

Equations

• ⋯ = ⋯

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

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