lintegral_toKernel_univ

Mathlib.Probability.Kernel.Disintegration.CDFToKernel

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.lintegral_toKernel_univ

← MathLib Explorer

English

If r ≤ r', then ρ.IicSnd r ≤ ρ.IicSnd r'.

Русский

Если r ≤ r', то ρ.IicSnd r ≤ ρ.IicSnd r'.

LaTeX

$$$\rho.IicSnd\, r \leq \rho.IicSnd\, r'\quad(\text{если } r \le r')$$$

Lean4

theorem lintegral_toKernel_univ [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν) (a : α) :
    ∫⁻ b, hf.toKernel f (a, b) univ ∂(ν a) = κ a univ := by
  rw [← setLIntegral_univ, setLIntegral_toKernel_univ hf a MeasurableSet.univ, univ_prod_univ]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru