English
If a measure ν agrees with μ on all cylinder boxes, then ν equals infinitePi μ.
Русский
Если мера ν совпадает с μ на всех цилиндрических коробках, тогда ν равно infinitePi μ.
LaTeX
$$$$\forall s, t, (∀ i, ...) \Rightarrow ν = \mathrm{infinitePi}\;μ.$$$$
Lean4
theorem infinitePi_map_pi {Y : ι → Type*} [∀ i, MeasurableSpace (Y i)] {f : (i : ι) → X i → Y i}
(hf : ∀ i, Measurable (f i)) :
haveI (i : ι) : IsProbabilityMeasure ((μ i).map (f i)) := isProbabilityMeasure_map (hf i).aemeasurable
(infinitePi μ).map (fun x i ↦ f i (x i)) = infinitePi (fun i ↦ (μ i).map (f i)) :=
by
have (i : ι) : IsProbabilityMeasure ((μ i).map (f i)) := isProbabilityMeasure_map (hf i).aemeasurable
refine eq_infinitePi _ fun s t ht ↦ ?_
rw [map_apply (by fun_prop) (.pi s.countable_toSet ht)]
have : (fun (x : Π i, X i) i ↦ f i (x i)) ⁻¹' ((s : Set ι).pi t) = (s : Set ι).pi (fun i ↦ (f i) ⁻¹' (t i)) := by
ext x; simp
rw [this, infinitePi_pi _ (fun i hi ↦ hf i (ht i hi))]
refine Finset.prod_congr rfl fun i hi ↦ ?_
rw [map_apply (by fun_prop) (ht i hi)]
