isRatCondKernelCDF_preCDF — Mathlib

English

For finite ρ, the function a ↦ (preCDF ρ r a)^{toReal} along with kernels Unit ρ and Unit ρ.fst satisfies IsRatCondKernelCDF; in particular, the construction yields a rational-conditioned CDF kernel for the preCDF.

Русский

Пусть ρ конечна; функция a ↦ (preCDF ρ r a)^{toReal} вместе с ядрами Unit ρ и Unit ρ.fst образуют IsRatCondKernelCDF; следовательно, получается рационально условное ядро для предCDF.

LaTeX

$$$IsRatCondKernelCDF\\left( a \\mapsto (\\mathrm{preCDF}(ρ, r, a))^{\\mathrm{toReal}} \\, , \\; Kernel.const\\ Unit\\, ρ , \\; Kernel.const\\ Unit\\, ρ.fst \\right).$$$

Lean4

theorem isRatCondKernelCDF_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    IsRatCondKernelCDF (fun p r ↦ (preCDF ρ r p.2).toReal) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst) :=
  (isRatCondKernelCDFAux_preCDF ρ).isRatCondKernelCDF

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