isRatCondKernelCDF_density_Iic — Mathlib

English

For hf, a, x ∈ ℝ, stieltjesOfMeasurableRat f hf a x ≤ 1.

Русский

Для hf, a и x ∈ ℝ справедливо: stieltjesOfMeasurableRat f hf a x ≤ 1.

LaTeX

$$$stieltjesOfMeasurableRat(f,hf,a)(x) \le 1$$$

Lean4

/-- Taking the kernel density of intervals `Iic q` for `q : ℚ` gives a function with the property
`isRatCondKernelCDF`. -/
theorem isRatCondKernelCDF_density_Iic (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    IsRatCondKernelCDF (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ) :=
  (isRatCondKernelCDFAux_density_Iic κ).isRatCondKernelCDF

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