setLIntegral_condKernel_eq_measure_prod

English

In the conditional-product decomposition, the left L-integral equals the product-measure along s×t.

Русский

В разложении по условному произведению левая L-интеграл равна произведению меры по s×t.

LaTeX

$$$\\forall a\\; s\\; t, \\; \\int_{b\\in s} ρ.condKernel b t \\; dρ.fst = ρ a (s ×ˢ t)$$$

Lean4

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

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