English
Reindexing coordinates by a bijection e yields an equivalent product measure: pushing forward the product measure along the natural coordinate permutation equals the product measure on the target indexing.
Русский
Перебиндирование координат по биекциям сохраняет произведение меры: перенесённая через естественную перестановку координат мера равно произведению по целевой индексации.
LaTeX
$$$\\bigl(\\mathrm{Measure.pi}\\; (\\lambda i.\\; \\mu (e(i)))\\bigr)\\text{ map } (\\mathrm{MeasurableEquiv.piCongrLeft} (\\lambda i.\\beta i) e) = \\mathrm{Measure.pi}\\; \\mu$$$
Lean4
theorem pi_map_piCongrLeft [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type*} [∀ i, MeasurableSpace (β i)]
(μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
(Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) = Measure.pi μ :=
by
let e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i ↦ β i) e
refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm
rw [e_meas.measurableEmbedding.map_apply]
let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i)
have : e_meas ⁻¹' pi univ s = pi univ s' := by
ext x
simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, s']
refine (e.forall_congr ?_).symm
intro i
rw [MeasurableEquiv.piCongrLeft_apply_apply e x i]
rw [this, pi_pi, Finset.prod_equiv e.symm]
· simp only [Finset.mem_univ, implies_true]
intro i _
simp only [s']
congr
all_goals rw [e.apply_symm_apply]
