lintegral_restrict_infinitePi — Mathlib

English

The lintegral over infinitePi of a function that depends only on finitely many coordinates equals the corresponding finite integral over the pi measure on those coordinates.

Русский

Линтеграл по infinitePi от функции, зависящей только от конечного наборa координат, равен соответствующему конечному интегралу по мере pi на этих координатах.

LaTeX

$$$$\int\! f \,d(\mathrm{infinitePi}\,μ) = \int\! f \; d\mathrm{pi}(μ)$$ на соответствующих ограничениях.$$

Lean4

theorem lintegral_restrict_infinitePi {s : Finset ι} {f : (Π i : s, X i) → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ y, f (s.restrict y) ∂infinitePi μ = ∫⁻ y, f y ∂Measure.pi (fun i : s ↦ μ i) := by
  rw [← lintegral_map hf (measurable_restrict _), isProjectiveLimit_infinitePi μ]

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