English
For κ, η as above, the first marginal of κ ⊗ η evaluated at x and measurable set s is the integral over b of the indicator of s under κ and η, i.e., equals ∫ b s.indicator η (x,b) Set.univ d(κ x).
Русский
Пусть κ, η – как выше; первая маргинальная часть κ ⊗ η по x равна интегралу по b от индикации s.
LaTeX
$$$$ (κ ⊗ₖ η)^{{\\text{fst}}} x\, s = \\int^\\!- b \\, s.{\\text{indicator}} (b) \\, η (x,b) \\; d(κ x). $$$$
Lean4
/-- If `η` is a Markov kernel, use instead `fst_compProd` to get `(κ ⊗ₖ η).fst = κ`. -/
theorem fst_compProd_apply (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (x : α)
{s : Set β} (hs : MeasurableSet s) : (κ ⊗ₖ η).fst x s = ∫⁻ b, s.indicator (fun b ↦ η (x, b) Set.univ) b ∂(κ x) :=
by
rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply]
swap; · exact measurable_fst hs
have h_eq b : η (x, b) {c | b ∈ s} = s.indicator (fun b ↦ η (x, b) Set.univ) b := by by_cases hb : b ∈ s <;> simp [hb]
simp_rw [Set.preimage, Set.mem_setOf_eq, h_eq]
