English
For any a, x0, and cylinder set s, trajContent κ x0 s ≠ ∞; in particular it is finite for measurable cylinders.
Русский
Для любого a, x0 и множества цилиндра s, trajContent κ x0 s не равна бесконечности; оно конечно на измеримых цилиндрах.
LaTeX
$$$\\forall a\\;\\forall x_0\\;\\forall s,\\ MeasurableSet\\; s\\Rightarrow\\ trajContent\\ κ\\ x_0\\ s \\neq \\infty$$$
Lean4
/-- The `trajContent` of a cylinder is equal to the integral of its indicator function against
`partialTraj`. -/
theorem trajContent_eq_lmarginalPartialTraj {b : ℕ} {S : Set (Π i : Iic b, X i)} (mS : MeasurableSet S) (x₀ : Π n, X n)
(a : ℕ) :
trajContent κ (frestrictLe a x₀) (cylinder (Iic b) S) =
lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x₀ :=
by
rw [trajContent_cylinder mS, ← lintegral_indicator_one mS, lmarginalPartialTraj]
congr with x
apply Set.indicator_const_eq_indicator_const
rw [mem_cylinder]
congrm (fun i ↦ ?_) ∈ S
simp [updateFinset, i.2]
