English
The unique index case yields a product measure preserving mapping from pi μ to μ(default).
Русский
В случае единственного индекса сохраняется меру при переходе от pi μ к μ(по умолчанию).
LaTeX
$$measurePreserving_piUnique (X) (μ) :$$
Lean4
theorem measurePreserving_piUnique {X : ι → Type*} [Unique ι] {m : ∀ i, MeasurableSpace (X i)}
(μ : ∀ i, Measure (X i)) : MeasurePreserving (MeasurableEquiv.piUnique X) (Measure.pi μ) (μ default)
where
measurable := (MeasurableEquiv.piUnique X).measurable
map_eq := by
set e := MeasurableEquiv.piUnique X
have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) :=
by
ext1 s
rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]
congr 1; exact e.toEquiv.image_eq_preimage s
simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self, toOuterMeasure_toMeasure,
MeasurableEquiv.map_map_symm]
