setIntegral_prod_mul — Mathlib

English

Fubini-type result for products restricted to sets: ∫ z in s×t, f z = ∫ x in s ∫ y in t, f(x,y).

Русский

Фубини-типовый результат для произведения ограниченного множества: интеграл по s×t равен двумерному интегралу по s и t.

LaTeX

$$$$\\int z \\in s \\times s t, f(z) \\; d(μ×ν) = \\int x \\in s, \\int y \\in t, f(x,y) \\, dν \\; dμ.$$$$

Lean4

theorem setIntegral_prod_mul {L : Type*} [RCLike L] (f : α → L) (g : β → L) (s : Set α) (t : Set β) :
    ∫ z in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ x in s, f x ∂μ) * ∫ y in t, g y ∂ν :=
  by
  rw [← Measure.prod_restrict s t]
  apply integral_prod_mul

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