English
If a measurable function f on trajectories is AEStronglyMeasurable with respect to traj κ a x0, then for every a ≤ b, f remains AEStronglyMeasurable when restricted to the truncated trajectory up to b, almost everywhere with respect to traj κ a x0.
Русский
Если f измеримо на траекториях и AEStronglyMeasurable относительно traj κ a x0, то при ограничении траектории до b f сохраняет AEStronglyMeasurable почти повсеместно относительно traj κ a x0.
LaTeX
$$$\\text{If } \\text{hab}: a \\le b,\\; x_0,\\; f \\text{ is AEStronglyMeasurable w.r.t. } \\operatorname{traj}_κ a x_0, \\\\forall\\text{ almost } x,\\; f \\text{ remains AEStronglyMeasurable under } \\operatorname{traj}_κ b (\\operatorname{frestrictLe} b x)$$$
Lean4
theorem aestronglyMeasurable_traj {a b : ℕ} (hab : a ≤ b) {f : (Π n, X n) → E} {x₀ : Π i : Iic a, X i}
(hf : AEStronglyMeasurable f (traj κ a x₀)) : ∀ᵐ x ∂partialTraj κ a b x₀, AEStronglyMeasurable f (traj κ b x) :=
by
rw [← traj_comp_partialTraj hab] at hf
exact hf.comp
