English
trajContent κ x0 evaluated on cylinder S equals lmarginalPartialTraj κ a b evaluated at x0 with the indicator of S: trajContent κ (frestrictLe a x0) (cylinder (Iic b) S) = lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x0
Русский
trajContent κ x0 на цилиндре S равно lmarginalPartialTraj κ a b, где применяется индикатор S к цилиндру.
LaTeX
$$$\\text{trajContent}\\;\\kappa\\; x_0\\; (\\text{cylinder } (Iic\\; b)\\; S) = \\text{lmarginalPartialTraj}\\;\\kappa\\; a\\; b\\; ((\\text{cylinder } (Iic\\; b)\\; S).\\textindicator 1)\\; x_0$$$
Lean4
/-- The `trajContent κ x₀` of a cylinder indexed by first coordinates is given by `partialTraj`. -/
theorem trajContent_cylinder {a b : ℕ} {S : Set (Π i : Iic b, X i)} (mS : MeasurableSet S) (x₀ : Π i : Iic a, X i) :
trajContent κ x₀ (cylinder (Iic b) S) = partialTraj κ a b x₀ S := by
rw [trajContent, projectiveFamilyContent_cylinder _ mS, inducedFamily_Iic]
