English
Let α be any type and μ, ν be measures on α with Sigma-finite condition. The finite two-arrow vector construction yields a volume-preserving map from the product measure to the product of μ and ν.
Русский
Пусть α — произвольное множество, μ и ν — меры на α с условием сигма-мфинитности. Конструкция FinTwoArrow vec даёт меропереносимый по объёму переход между произведением и произведением мер μ×ν.
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.finTwoArrow}(\,[μ,ν]\!)\bigr)\; (\mathrm{Measure.pi}\, ![μ,ν])\; (μ \mathrm{.prod} ν) $$$
Lean4
theorem measurePreserving_finTwoArrow_vec {α : Type u} {_ : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ]
[SigmaFinite ν] : MeasurePreserving MeasurableEquiv.finTwoArrow (Measure.pi ![μ, ν]) (μ.prod ν) :=
haveI : ∀ i, SigmaFinite (![μ, ν] i) := Fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩
measurePreserving_piFinTwo _
