compProd_apply_prod — Mathlib

English

If κ and η are S-finite kernels, then for a measurable s ⊆ β, t ⊆ γ, (κ ⊗ₖ η) a (s × t) = ∫_{b∈s} η(a,b)(t) dκ(a)(b).

Русский

Для измеримых s ⊆ β и t ⊆ γ имеем (κ ⊗ₖ η) a (s × t) = ∫_{b∈s} η(a,b)(t) dκ(a)(b).

LaTeX

$$$$ (κ \otimes_k η) a (s \times^\mathrm{S} t) = \int_{b \in s} η(a,b)(t) \, dκ(a)(b). $$$$

Lean4

theorem compProd_apply_prod {κ : Kernel α β} {η : Kernel (α × β) γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] {a : α}
    {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
    (κ ⊗ₖ η) a (s ×ˢ t) = ∫⁻ b in s, η (a, b) t ∂(κ a) :=
  by
  rw [compProd_apply (hs.prod ht), ← lintegral_indicator hs]
  congr with a
  by_cases ha : a ∈ s <;> simp [ha]

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