English
If a function f is integrable with respect to traj κ a x0, then for almost every x in traj up to a, f remains integrable along the extended trajectory to b, after adjusting via frestrictLe and x.
Русский
Если функция f интегрируема по траектории, то для почти каждой точки траектории до a интегрируемость сохраняется при продолжении траектории до b после корректировок frestrictLe.
LaTeX
$$$\\text{If } a \\le b,\\; x_0,\\; \\text{and } i_f: \\text{Integrable}(f, \\operatorname{traj}_κ a x_0) \\Rightarrow \n\\quad \\forall\\text{ almost } x \\; (\\operatorname{traj}_κ a x_0), \\; \\text{Integrable}(f, \\operatorname{traj}_κ b (\\operatorname{frestrictLe} b x))$$$
Lean4
theorem integrable_traj {a b : ℕ} (hab : a ≤ b) {f : (Π n, X n) → E} (x₀ : Π i : Iic a, X i)
(i_f : Integrable f (traj κ a x₀)) : ∀ᵐ x ∂traj κ a x₀, Integrable f (traj κ b (frestrictLe b x)) :=
by
rw [← traj_comp_partialTraj hab, integrable_comp_iff] at i_f
· apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))
· fun_prop
· convert i_f.1
rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]
· exact i_f.aestronglyMeasurable
