lintegral_condKernel_mem — Mathlib

English

For a finite measure ρ on β×Ω, the integral over the base fst of the conditional kernel against a set s recovers the measure ρ on s.

Русский

Для конечной меры ρ на β×Ω интеграл по fst условного ядра против множества s восстанавливает меру ρ на s.

LaTeX

$$$\\int x,\\; ρ.condKernel x {y | (x,y) ∈ s} \\; dρ.fst = ρ s$$$

Lean4

theorem lintegral_condKernel_mem {s : Set (β × Ω)} (hs : MeasurableSet s) :
    ∫⁻ x, ρ.condKernel x {y | (x, y) ∈ s} ∂ρ.fst = ρ s :=
  by
  conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  simp_rw [compProd_apply hs]
  rfl

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