English
For a fixed a and x0, and a measurable function f on the trajectory, the nonnegative integral with respect to traj κ a x0 equals the integral of f applied to the updated trajectory, i.e., replacing x by updateFinset x on Iic a inside the trajectory.
Русский
Для фиксированных a и x0 и измеримой функции f по траектории, линтеграл по траектории равен лингентегралу после замены x на обновленный на Iic a траекторий.
LaTeX
$$$\\int^{-}_{x} f(x) \, d\\operatorname{traj}_κ a x_0 = \\int^{-}_{x} f(\\operatorname{updateFinset} x (\\mathsf{Iic}\\,a) x_0) \\, d\\operatorname{traj}_κ a x_0$$$
Lean4
theorem lintegral_traj₀ {a : ℕ} (x₀ : Π i : Iic a, X i) {f : (Π n, X n) → ℝ≥0∞} (mf : AEMeasurable f (traj κ a x₀)) :
∫⁻ x, f x ∂traj κ a x₀ = ∫⁻ x, f (updateFinset x (Iic a) x₀) ∂traj κ a x₀ :=
by
nth_rw 1 [← traj_map_updateFinset, MeasureTheory.lintegral_map']
· convert mf
exact traj_map_updateFinset x₀
· exact measurable_updateFinset_left.aemeasurable
