English
If f is integrable with respect to traj κ a x0, then the iterated integral over traj κ b x and partialTraj κ a b x0 equals the integral of f over traj κ a x0 after appropriate variable rearrangement.
Русский
Если f интегрируемо по траектории, то двойной интеграл по traj κ b x и partialTraj κ a b x0 эквивалентен интегралу f по traj κ a x0 после корректного обращения переменных.
LaTeX
$$$\\int_x \\int_y f(x,y) \\; d(\\operatorname{traj}_κ b x) \\, d(\\partial_κ a b x_0) = \\int_x f(\\operatorname{frestrictLe} b x, x) \\, d(\\operatorname{traj}_κ a x_0)$$$
Lean4
theorem integral_traj_partialTraj {a b : ℕ} (hab : a ≤ b) {x₀ : Π i : Iic a, X i} {f : (Π n : ℕ, X n) → E}
(hf : Integrable f (traj κ a x₀)) : ∫ x, ∫ y, f y ∂traj κ b x ∂partialTraj κ a b x₀ = ∫ x, f x ∂traj κ a x₀ :=
by
apply integral_traj_partialTraj' hab
rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
exact hf.comp_measurable measurable_snd
