English
Let f be a function on the product α × β taking values in a normed space E. Then f is integrable with respect to the product measure μ × ν if and only if the composed function f ∘ Prod.swap is integrable with respect to the swapped product ν × μ. This is a symmetry of integrability under swapping the coordinates.
Русский
Пусть f — функция на произведении α × β, принимающая значения в нормированном пространстве E. Тогда f интегрируема по произведению меры μ × ν тогда и только тогда, когда композиция f с перестановкой координат f ∘ Prod.swap интегрируема по произведению ν × μ. Это симметрия интегрируемости при перестановке координат.
LaTeX
$$$\\mathrm{Integrable}(f \\circ \\mathrm{Prod.swap})\\ (\\nu \\times \\mu) \\iff \\mathrm{Integrable}(f)\\ (\\mu \\times \\nu)$$$
Lean4
theorem integrable_swap_iff [SFinite μ] {f : α × β → E} :
Integrable (f ∘ Prod.swap) (ν.prod μ) ↔ Integrable f (μ.prod ν) :=
measurePreserving_swap.integrable_comp_emb MeasurableEquiv.prodComm.measurableEmbedding
