toKernel_Iic — Mathlib

English

For any p = (a, b) and any x ∈ ℝ, the probability of the interval (−∞, x] under hf.toKernel f at p equals ENNReal.ofReal (f p x).

Русский

Для любого p = (a, b) и любого x ∈ ℝ вероятность для интервала (−∞, x] под hf.toKernel f в точке p равна ENNReal.ofReal (f p x).

LaTeX

$$$hf.toKernel f\, p\ (Iic\ x) = \mathrm{ENNReal}.ofReal\left((f\, p)\, x\right)$$$

Lean4

theorem toKernel_Iic {hf : IsCondKernelCDF f κ ν} (p : α × β) (x : ℝ) :
    hf.toKernel f p (Iic x) = ENNReal.ofReal (f p x) :=
  by
  rw [IsCondKernelCDF.toKernel_apply p, (f p).measure_Iic (hf.tendsto_atBot_zero p)]
  simp

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