integral_fin_nat_prod_volume_eq_prod

English

A version of Fubini for finite n using volume measures: the integral over the product space with respect to the volume-based product measure equals the product of the single-variable integrals (also with volume).

Русский

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

LaTeX

$$$$\\int x:(i:Fin\\,n)\\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** in `n` variables, for a natural number `n`. -/
theorem integral_fin_nat_prod_volume_eq_prod {n : ℕ} {E : Fin n → Type*} [∀ i, MeasureSpace (E i)]
    [∀ i, SigmaFinite (volume : Measure (E i))] (f : (i : Fin n) → E i → 𝕜) :
    ∫ x : (i : Fin n) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x :=
  integral_fin_nat_prod_eq_prod _

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