English
Value of infinitePi on a cylinder set equals the product of marginals over the index set: infinitePi μ (cylinder s S) = ∏ i∈s μ_i(S_i).
Русский
Значение infinitePi на цилиндре равно произведению маргинал по индексу: infinitePi μ (cylinder s S) = ∏_{i∈s} μ_i(S_i).
LaTeX
$$$$\text{infinitePi}_{i} (μ_i)(\text{cylinder } sS) = \prod_{i∈s} μ_i(S_i).$$$$
Lean4
theorem infinitePi_pi {s : Finset ι} {t : (i : ι) → Set (X i)} (mt : ∀ i ∈ s, MeasurableSet (t i)) :
infinitePi μ (Set.pi s t) = ∏ i ∈ s, (μ i) (t i) :=
by
have : Set.pi s t = cylinder s ((@Set.univ s).pi (fun i : s ↦ t i)) :=
by
ext x
simp
rw [this, cylinder, ← map_apply, infinitePi_map_restrict, pi_pi]
· rw [univ_eq_attach, prod_attach _ (fun i ↦ (μ i) (t i))]
· exact measurable_restrict _
· exact .univ_pi fun i ↦ mt i.1 i.2
