compProd_apply_prod — Mathlib

English

For SFinite μ and an SFinite kernel κ, the product measure of a rectangle s × t equals the integral over s of κ(a)(t) with respect to μ.

Русский

При SFinite μ и ядре κ с конечной массой мер на каждом a, мера прямоугольника s × t равна интегралу по a∈s от κ(a)(t) по μ.

LaTeX

$$$[\\mathrm{SFinite}\\; μ] [\\mathrm{IsSFiniteKernel}\\; κ] \\; {s : \\mathrm{Set} \\alpha} {t : \\mathrm{Set} \\beta} (hs : \\mathrm{MeasurableSet}\\; s) (ht : \\mathrm{MeasurableSet}\\; t) : (μ ⊗_m κ)(s \\times^\\! t) = \\int^- a \\in s, κ a t \\partial μ$$$

Lean4

theorem compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ] {s : Set α} {t : Set β} (hs : MeasurableSet s)
    (ht : MeasurableSet t) : (μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ a in s, κ a t ∂μ := by
  simp [compProd, Kernel.compProd_apply_prod hs ht]

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