integral_restrict_infinitePi — Mathlib

English

Integrals over infinitePi can be computed by integrating over the product measure π on the index set via a suitable change of variables.

Русский

Интегралы по infinitePi можно считать интегрированием по произведению π на индексе через соответствующее преобразование переменных.

LaTeX

$$$$\int f \,d(\mathrm{infinitePi}\,μ) = \int f \circ \text{update}_{\text{Finset}} \; d\mathrm{pi}(μ).$$$$

Lean4

theorem integral_restrict_infinitePi {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι}
    {f : (Π i : s, X i) → E} (hf : AEStronglyMeasurable f (Measure.pi (fun i : s ↦ μ i))) :
    ∫ y, f (s.restrict y) ∂infinitePi μ = ∫ y, f y ∂Measure.pi (fun i : s ↦ μ i) :=
  by
  rw [← integral_map, infinitePi_map_restrict]
  · fun_prop
  · rwa [infinitePi_map_restrict]

Похожие утверждения