isCondKernelCDF_stieltjesOfMeasurableRat

English

From IsCondKernelCDF one builds a Markov kernel from α×β to ℝ by assigning to p the measure given by f(p).

Русский

Из IsCondKernelCDF строится марковское ядро из α×β в ℝ, задавая для p меру f(p).

LaTeX

$$$\text{toKernel}(f, hf)\;:\; (α×β) \to\mathcal{P}(\mathbb{R})$ with $\bigl(\text{toKernel}(f, hf)\bigr)(p) = (f(p)).\text{measure}$.$$

Lean4

theorem isCondKernelCDF_stieltjesOfMeasurableRat {f : α × β → ℚ → ℝ} (hf : IsRatCondKernelCDF f κ ν)
    [IsFiniteKernel κ] : IsCondKernelCDF (stieltjesOfMeasurableRat f hf.measurable) κ ν
    where
  measurable := measurable_stieltjesOfMeasurableRat hf.measurable
  integrable := integrable_stieltjesOfMeasurableRat hf
  tendsto_atTop_one := tendsto_stieltjesOfMeasurableRat_atTop hf.measurable
  tendsto_atBot_zero := tendsto_stieltjesOfMeasurableRat_atBot hf.measurable
  setIntegral a _ hs x := setIntegral_stieltjesOfMeasurableRat hf a x hs

Похожие утверждения