English
Pushing forward the product measure by a reindexing equivalence yields the reindexed product measure, consistent with piContent on cylinders.
Русский
Перемещение по переиндексации ядра продукта даёт переиндексированное произведение меры, согласующееся с piContent по цилиндрам.
LaTeX
$$$$\mathrm{infinitePiNat}\;\bigl(\lambda n.\mu(e(n))\bigr)\mapsto \mathrm{piCongrLeft}\;X\;e = \mathrm{infinitePi}\;\mu.$$$$
Lean4
/-- If we push the product measure forward by a reindexing equivalence, we get a product measure
on the reindexed product in the sense that it coincides with `piContent μ` over
measurable cylinders. See `infinitePi_map_piCongrLeft` for a general version. -/
theorem infinitePiNat_map_piCongrLeft (e : ℕ ≃ ι) {s : Set (Π i, X i)} (hs : s ∈ measurableCylinders X) :
(infinitePiNat (fun n ↦ μ (e n))).map (piCongrLeft X e) s = piContent μ s :=
by
obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders s).1 hs
rw [map_apply _ hS.cylinder, cylinder, ← Set.preimage_comp, coe_piCongrLeft, restrict_comp_piCongrLeft,
Set.preimage_comp, ← map_apply, infinitePiNat_map_restrict (fun n ↦ μ (e n)), ← cylinder, piContent_cylinder μ hS, ←
pi_map_piCongrLeft (e.restrictPreimageFinset I), map_apply _ hS, coe_piCongrLeft]
· simp
any_goals fun_prop
exact hS.preimage (by fun_prop)
