integral_fintype_prod_volume_eq_prod

English

If each E_i has a volume measure, then the Fubini-type equality holds with volume-based integrals: ∫ ∏ f_i(x_i) dπ(volume) = ∏ ∫ f_i dμ_i(volume).

Русский

Для пространства с мерами объема выполняется равенство Фубини для объема: интеграл произведения равен произведению интегралов по объему.

LaTeX

$$$$\\int x:(i:\\iota)\\to E_i,\\; \\prod_i f_i(x_i)\\,d(\\operatorname{pi.volume}\\;\\mu)=\\prod_i\\int x, f_i(x)\\,d(\\mu_i).volume$$$$

Lean4

/-- A version of **Fubini's theorem** with the variables indexed by a general finite type. -/
theorem integral_fintype_prod_volume_eq_prod {E : ι → Type*} (f : (i : ι) → E i → 𝕜) [∀ i, MeasureSpace (E i)]
    [∀ i, SigmaFinite (volume : Measure (E i))] : ∫ x : (i : ι) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x :=
  integral_fintype_prod_eq_prod _

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