lintegral_prod_symm — Mathlib

English

Symmetric version: if f and g are quasi-measure-preserving, then Prod.map f g preserves the product measures in the symmetric setup.

Русский

Симметричная версия: если f и g сохраняют меру, то Prod.map f g сохраняет произведение мер в симметрной постановке.

LaTeX

$$QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)$$

Lean4

/-- The symmetric version of Tonelli's Theorem: For `ℝ≥0∞`-valued almost everywhere measurable
functions on `α × β`, the integral of `f` is equal to the iterated integral, in reverse order. -/
theorem lintegral_prod_symm [SFinite μ] (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.prod ν)) :
    ∫⁻ z, f z ∂μ.prod ν = ∫⁻ y, ∫⁻ x, f (x, y) ∂μ ∂ν :=
  by
  simp_rw [← lintegral_prod_swap f]
  exact lintegral_prod _ hf.prod_swap

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