English
If f and g are quasi-measure-preserving between μ→ν and τ→υ, then Prod.map f g is quasi-measure-preserving from μ.prod τ to ν.prod υ.
Русский
Если f и g сохраняют меру в отношении μ→ν и τ→υ, то Prod.map f g сохраняет меру между μ×τ и ν×υ.
LaTeX
$$QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)$$
Lean4
/-- **Tonelli's Theorem for set integrals**: For `ℝ≥0∞`-valued almost everywhere measurable
functions on `s ×ˢ t`, the integral of `f` on `s ×ˢ t` is equal to the iterated integral on `s`
and `t` respectively. -/
theorem setLIntegral_prod [SFinite μ] {s : Set α} {t : Set β} (f : α × β → ℝ≥0∞)
(hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))) :
∫⁻ z in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ x in s, ∫⁻ y in t, f (x, y) ∂ν ∂μ := by
rw [← Measure.prod_restrict, lintegral_prod _ (by rwa [Measure.prod_restrict])]
