English
For measurable s ⊆ β, (κ ⊗ₖ η) x (fst^{-1}(s)) = κ x s.
Русский
Для измеримого s ⊆ β выполняется (κ ⊗ₖ η) x (fst^{-1}(s)) = κ x s.
LaTeX
$$$$ (\kappa \otimes_k \eta)(x)(\operatorname{fst}^{-1}(s)) = \kappa(x)(s). $$$$
Lean4
theorem compProd_preimage_fst {s : Set β} (hs : MeasurableSet s) (κ : Kernel α β) (η : Kernel (α × β) γ)
[IsSFiniteKernel κ] [IsMarkovKernel η] (x : α) : (κ ⊗ₖ η) x (Prod.fst ⁻¹' s) = κ x s := by
classical
simp_rw [compProd_apply (measurable_fst hs), ← Set.preimage_comp, Prod.fst_comp_mk, Set.preimage,
Function.const_apply]
have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b :=
by
intro b
by_cases hb : b ∈ s <;> simp [hb]
simp_rw [this]
rw [lintegral_indicator_const hs, one_mul]