English
For measurable f, the lintegral over infinitePi μ of f equals the lintegral over pi μ on the finite index set after a suitable change of variables.
Русский
Для измеримой функции f линтеграл по infinitePi μ равен линергралу по pi μ на конечном индексе после корректного преобразования переменных.
LaTeX
$$$$\int f \, d(\mathrm{infinitePi}\,μ) = \int f \circ \text{updateFinset} \; d\mathrm{pi}(μ).$$$$
Lean4
theorem lintegral_infinitePi_of_piFinset [DecidableEq ι] {s : Finset ι} {f : (Π i, X i) → ℝ≥0∞}
(mf : Measurable[piFinset s] f) (x : Π i, X i) : ∫⁻ y, f y ∂infinitePi μ = (∫⋯∫⁻_s, f ∂μ) x :=
by
let g : (Π i : s, X i) → ℝ≥0∞ := 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 [← lintegral_congr_ae <| ae_of_all _ this, lintegral_restrict_infinitePi]
· rfl
· exact mf.comp (measurable_updateFinset.mono le_rfl (piFinset.le s))
