English
Integral over infinitePi of a function on a finite index set equals the iterated integral over the finite marginals.
Русский
Интеграл по infinitePi над функцией на конечном индексе равен последовательному интегралу над маргиналами.
LaTeX
$$$$\int f \, d\mathrm{infinitePi}\;μ = \int f \, d\mathrm{pi}(μ|_{\mathrm{finite}}).$$$$
Lean4
theorem integral_infinitePi_of_piFinset [DecidableEq ι] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{s : Finset ι} {f : (Π i, X i) → E} (mf : StronglyMeasurable[piFinset s] f) (x : Π i, X i) :
∫ y, f y ∂infinitePi μ = ∫ y, f (Function.updateFinset x s y) ∂Measure.pi (fun i : s ↦ μ i) :=
by
let g : (Π i : s, X i) → E := fun y ↦ f (Function.updateFinset x _ y)
have this y : g (s.restrict y) = f y := mf.dependsOn_of_piFinset fun i hi ↦ by simp_all [Function.updateFinset]
rw [← integral_congr_ae <| ae_of_all _ this, integral_restrict_infinitePi]
exact mf.comp_measurable (measurable_updateFinset.mono le_rfl (piFinset.le s)) |>.aestronglyMeasurable
