English
As before, piContent tends to zero along a decreasing sequence of cylinders with empty intersection, establishing sigma-subadditivity and extension to a larger sigma-algebra.
Русский
Как и прежде, piContent стремится к нулю вдоль убывающей последовательности цилиндров с пустым пересечением, что устанавливает сигма-аддитивность и развёртывание на большую сигма-алгебру.
LaTeX
$$$$\mathrm{Tendsto}\bigl(n \mapsto \piContent(μ)(A_n)\bigr)\to 0.$$$$
Lean4
theorem _root_.measurePreserving_eval_infinitePi (i : ι) : MeasurePreserving (Function.eval i) (infinitePi μ) (μ i)
where
measurable := by fun_prop
map_eq := by
ext s hs
have :
@Function.eval ι X i = (@Function.eval ({ i } : Finset ι) (fun j ↦ X j) ⟨i, by simp⟩) ∘ (Finset.restrict { i }) :=
by ext; simp
rw [this, ← map_map, infinitePi_map_restrict, (measurePreserving_eval _ _).map_eq]
all_goals fun_prop
