setIntegral_prod — Mathlib

English

If L is a continuous linear map on E×F to G, and the projections are integrable, then L is integrable on μ×ν.

Русский

Пусть L — непрерывное линейное отображение E×F→G, и проекции интегрируемы; тогда L интегрируема по произведению μ×ν.

LaTeX

$$$$\\text{Integrable } L(μ×ν) \\Rightarrow \\text{Integrable } L \\text{ on } μ×ν.$$$$

Lean4

/-- **Fubini's Theorem** for set integrals. -/
theorem setIntegral_prod (f : α × β → E) {s : Set α} {t : Set β} (hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)) :
    ∫ z in s ×ˢ t, f z ∂μ.prod ν = ∫ x in s, ∫ y in t, f (x, y) ∂ν ∂μ :=
  by
  simp only [← Measure.prod_restrict s t, IntegrableOn] at hf ⊢
  exact integral_prod f hf

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