lintegral_condKernel_mem — Mathlib

English

Same as above, with a slightly different presentation of the measurability and integrability hypotheses; the equality of L-integrals holds.

Русский

То же самое предложение в иной формулировке условий измеримости и интегрируемости; равенство L-интегралов сохраняется.

LaTeX

$$$\\forall a, \\; \\int_{s} κ(a,b,t) \\, db = κ a(s\\times t)$$$

Lean4

theorem lintegral_condKernel_mem (a : α) {s : Set (β × Ω)} (hs : MeasurableSet s) :
    ∫⁻ x, Kernel.condKernel κ (a, x) (Prod.mk x ⁻¹' s) ∂(Kernel.fst κ a) = κ a s :=
  by
  conv_rhs => rw [← κ.disintegrate κ.condKernel]
  simp_rw [Kernel.compProd_apply hs]

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