setIntegral_prod_swap — Mathlib

English

Replacing the unrestriced integral by restricted measures, the equality holds for the swapped product as well.

Русский

Замена интеграла на ограниченный интеграл сохраняет равенство для переставленного произведения меры.

LaTeX

$$$\int z \ f(z.swap) \, d((ν×μ).restrict(S)) = \int z \ f(z) \, d((μ×ν).restrict(S'))$$$

Lean4

theorem setIntegral_prod_swap (s : Set α) (t : Set β) (f : α × β → E) :
    ∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ = ∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν := by
  rw [← Measure.prod_restrict, ← Measure.prod_restrict, integral_prod_swap]

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