English
A finite-variable version of Fubini: for n ∈ ℕ and f_i: E_i → 𝕜 with appropriate σ-finite measures μ_i, the integral over the product equals the product of the integrals.
Русский
Версия Фубини для конечного числа переменных: интеграл по произведению пространства равен произведению интегралов.
LaTeX
$$$$\\int x:(i:\\mathsf{Fin}\\,n)\\to E_i,\\; \\prod_i f_i(x_i)\\,d(\\pi\\mu)=\\prod_i\\int x, f_i(x)\\,d(\\mu_i).$$$$
Lean4
/-- A version of **Fubini's theorem** in `n` variables, for a natural number `n`. -/
theorem integral_fin_nat_prod_eq_prod {n : ℕ} {E : Fin n → Type*} {mE : ∀ i, MeasurableSpace (E i)}
{μ : (i : Fin n) → Measure (E i)} [∀ i, SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜) :
∫ x : (i : Fin n) → E i, ∏ i, f i (x i) ∂(Measure.pi μ) = ∏ i, ∫ x, f i x ∂(μ i) := by
induction n with
| zero => simp [measureReal_def]
| succ n n_ih =>
calc
_ =
∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i) ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) :=
by
rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv, Fin.prod_univ_succ, Fin.insertNth_zero,
Equiv.coe_fn_mk, Fin.cons_succ, Fin.zero_succAbove, cast_eq, Fin.cons_zero]
_ = (∫ x, f 0 x ∂μ 0) * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
rw [← n_ih, ← integral_prod_mul]
_ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]
