English
For a finite index set and a family of functions f_i: E_i → 𝕜, the integral of the product equals the product of the integrals: ∫ ∏_i f_i(x_i) dπμ = ∏_i ∫ f_i dμ_i.
Русский
Для конечного множества индексов и семейства функций выполняется равенство интегралов над произведением функций и произведение интегралов по каждому направлению.
LaTeX
$$$$\\int x:(i:\\iota)\\to E_i,\\; \\prod_i f_i(x_i)\\,d(\\operatorname{pi}\\;\\mu)=\\prod_i\\int x, f_i(x)\\,d(\\mu_i).$$$$
Lean4
/-- A version of **Fubini's theorem** with the variables indexed by a general finite type. -/
theorem integral_fintype_prod_eq_prod {E : ι → Type*} (f : (i : ι) → E i → 𝕜) {mE : ∀ i, MeasurableSpace (E i)}
{μ : (i : ι) → Measure (E i)} [∀ i, SigmaFinite (μ i)] :
∫ x : (i : ι) → E i, ∏ i, f i (x i) ∂(Measure.pi μ) = ∏ i, ∫ x, f i x ∂(μ i) :=
by
let e := (equivFin ι).symm
rw [← (measurePreserving_piCongrLeft _ e).integral_comp']
simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
MeasureTheory.integral_fin_nat_prod_eq_prod]
