lintegral_prod_swap — Mathlib

English

The order of integration can be swapped in the product Lintegral: ∫ f z.swap dν×μ = ∫ f z dμ×ν.

Русский

Можно поменять порядок интегрирования в произведении: ∫ f(z.swap) dν×μ = ∫ f(z) dμ×ν.

LaTeX

$$$\int f(z.swap) \, d(\nu \times \mu) = \int f(z) \, d(\mu \times \nu)$$$

Lean4

theorem lintegral_prod_swap [SFinite μ] (f : α × β → ℝ≥0∞) : ∫⁻ z, f z.swap ∂ν.prod μ = ∫⁻ z, f z ∂μ.prod ν :=
  measurePreserving_swap.lintegral_comp_emb MeasurableEquiv.prodComm.measurableEmbedding f

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