setLIntegral_toKernel_Iic — Mathlib

English

For a fixed a and x, integrating hf.toKernel f (a, b) (Iic x) over a measurable set s with respect to ν a gives κ a (s × Iic x).

Русский

Для фиксированного a и x интегрирование hf.toKernel f (a, b) (Iic x) по мере ν a по множеству измеримому s даёт κ a (s × Iic x).

LaTeX

$$$\int^{\llbracket b \rrbracket}_{b \in s} hf.toKernel f (a, b) (Iic x)\, \partial(\nu a) = κ a (s \times Iic x)$$$

Lean4

theorem setLIntegral_toKernel_Iic [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β}
    (hs : MeasurableSet s) : ∫⁻ b in s, hf.toKernel f (a, b) (Iic x) ∂(ν a) = κ a (s ×ˢ Iic x) :=
  by
  simp_rw [IsCondKernelCDF.toKernel_Iic]
  exact hf.setLIntegral _ hs _

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