English
For finite index ι and functions f_i, the substituted i-th component evaluation gives equality between a full product integral and the product of single integrals.
Русский
Для конечного индекса ι и функций f_i равенство между полным интегралом по произведению и произведением отдельных интегралов.
LaTeX
$$$$\\int x:(i:\\mathsf{Fin}\\,n)\\to E_i,\\; \\prod_i f_i(x_i)\\,d(\\operatorname{Measure.pi} \\mu)=\\prod_i\\int x, f_i(x)\\,d(\\mu_i).$$$$
Lean4
theorem integral_comp_eval [NormedSpace ℝ E] [∀ i, IsProbabilityMeasure (μ i)] {i : ι} {f : X i → E}
(hf : AEStronglyMeasurable f (μ i)) : ∫ x : Π i, X i, f (x i) ∂Measure.pi μ = ∫ x, f x ∂μ i :=
by
rw [← (measurePreserving_eval μ i).map_eq, integral_map]
· exact Measurable.aemeasurable (by fun_prop)
· rwa [(measurePreserving_eval μ i).map_eq]
