setLIntegral_condKernel_eq_measure_prod

English

In a measure-theoretic reformulation: the L-integral over s of the conditional kernel equals the measure of the product s×t under κ a.

Русский

В рамках теории меры: L-интеграл по s условного ядра равен мере множества s×t по κ a.

LaTeX

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

Lean4

theorem setLIntegral_condKernel_eq_measure_prod (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set Ω}
    (ht : MeasurableSet t) : ∫⁻ b in s, Kernel.condKernel κ (a, b) t ∂(Kernel.fst κ a) = κ a (s ×ˢ t) :=
  by
  have : κ a (s ×ˢ t) = (Kernel.fst κ ⊗ₖ Kernel.condKernel κ) a (s ×ˢ t) := by congr; exact (κ.disintegrate _).symm
  rw [this, Kernel.compProd_apply (hs.prod ht)]
  classical
  have : ∀ b, Kernel.condKernel κ (a, b) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b ↦ Kernel.condKernel κ (a, b) t) b :=
    by
    intro b
    by_cases hb : b ∈ s <;> simp [hb]
  simp_rw [Set.preimage, this]
  rw [lintegral_indicator hs]

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