instIsCondKernel — Mathlib

English

The condKernel of a finite kernel is a CondKernel.

Русский

У condKernel конечного ядра является CondKernel.

LaTeX

$$$κ.condKernel \\text{ is CondKernel}$$$

Lean4

instance _root_.MeasureTheory.Measure.condKernel.instIsCondKernel (ρ : Measure (α × Ω)) [IsFiniteMeasure ρ] :
    ρ.IsCondKernel ρ.condKernel where
  disintegrate :=
    by
    have h1 : const Unit (Measure.fst ρ) = fst (const Unit ρ) :=
      by
      ext
      simp only [fst_apply, Measure.fst, const_apply]
    have h2 : prodMkLeft Unit (Measure.condKernel ρ) = condKernelUnitBorel (const Unit ρ) :=
      by
      ext
      simp only [prodMkLeft_apply, Measure.condKernel_apply]
    rw [Measure.compProd, h1, h2, disintegrate]
    simp

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