English
trajContent κ x0 is sigma-subadditive with respect to the cylinder sigma-algebra; equivalently, it is additive across countable unions of disjoint cylinders.
Русский
trajContent κ x0 является сигмас-суваддитивным относительно цилиндрической сигма-алгебры; эквивалентно аддитивности по счетному объединению непересекающихся цилиндров.
LaTeX
$$$(trajContent\\;\\kappa\\; x_0).IsSigmaSubadditive$$$
Lean4
/-- The `trajContent` is sigma-subadditive. -/
theorem isSigmaSubadditive_trajContent {a : ℕ} (x₀ : Π i : Iic a, X i) : (trajContent κ x₀).IsSigmaSubadditive :=
by
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)
refine
addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders (trajContent κ x₀)
(fun _ _ ↦ trajContent_ne_top) ?_ hf hf_Union hf'
exact fun s hs anti_s inter_s ↦ trajContent_tendsto_zero hs anti_s inter_s x₀
