English
For an integrable trajectory functional f, the integral with respect to traj κ a x0 equals the integral of f evaluated on the updated trajectory after replacing the first a coordinates.
Русский
Для интегрируемого функционала траекторий интеграл по траектории равен интегралу от f на обновленной траектории после замены первых a координат.
LaTeX
$$$\\text{If } f \\text{ is integrable w.r.t. } \\operatorname{traj}_κ a x_0, \\int f \\, d\\operatorname{traj}_κ a x_0 = \\int f(\\operatorname{updateFinset}(x, \\mathsf{Iic}\\,a) x_0) \\, d\\operatorname{traj}_κ a x_0$$$
Lean4
/-- When computing `∫ x, f x ∂traj κ n x₀`, because the trajectory up to time `n` is
determined by `x₀` we can replace `x` by `updateFinset x (Iic a) x₀`. -/
theorem integral_traj {a : ℕ} (x₀ : Π i : Iic a, X i) {f : (Π n, X n) → E} (mf : AEStronglyMeasurable 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, integral_map]
· exact measurable_updateFinset_left.aemeasurable
· convert mf
rw [traj_map_updateFinset]
