English
Given an index equivalence f, the pi-congruence left map preserves the product measure after rearranging indices by f.
Русский
При наличии эквивалентности индексов f, левое перестановочное отображение pi сохраняет произведение мер после перестановки индексов by f.
LaTeX
$$measurePreserving_piCongrLeft(α, f)$$
Lean4
theorem measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableSpace β] [Fintype γ]
(μ : γ → Measure α) (ν : γ → Measure β) [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite (ν i)] :
MeasurePreserving (MeasurableEquiv.arrowProdEquivProdArrow α β γ) (.pi fun i ↦ (μ i).prod (ν i))
((Measure.pi fun i ↦ μ i).prod (Measure.pi fun i ↦ ν i))
where
measurable := (MeasurableEquiv.arrowProdEquivProdArrow α β γ).measurable
map_eq :=
by
refine
(FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
(FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)))
?_).symm
· refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm
· exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning
· exact (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)).isCountablySpanning
· rintro _ ⟨s, ⟨s, _, rfl⟩, ⟨_, ⟨t, _, rfl⟩, rfl⟩⟩
rw [MeasurableEquiv.map_apply, MeasurableEquiv.arrowProdEquivProdArrow, MeasurableEquiv.coe_mk]
rw [show Equiv.arrowProdEquivProdArrow γ _ _ ⁻¹' (univ.pi s ×ˢ univ.pi t) = (univ.pi fun i ↦ s i ×ˢ t i) by ext;
simp [Set.mem_pi, forall_and]]
simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]
