English
A variant form of the trajectory integral expresses the same law by restricting the integration to a measurable set and shifting the restriction via Set.preimage.
Русский
Вариант интеграла по траектории выражает ту же меру, ограничивая интегрирование до измеримого множества и смещая ограничение через preimage.
LaTeX
$$$\\int_{A} f \\, d\\operatorname{traj}_κ b x \\, d(\\partial_κ a b x_0) = \\int_{\\operatorname{preimage}(\\operatorname{frestrictLe} b, A)} f(\\cdot) \\, d\\operatorname{traj}_κ a x_0$$$
Lean4
theorem setIntegral_traj_partialTraj {a b : ℕ} (hab : a ≤ b) {x₀ : (Π i : Iic a, X i)} {f : (Π n : ℕ, X n) → E}
(hf : Integrable f (traj κ a x₀)) {A : Set (Π i : Iic b, X i)} (hA : MeasurableSet A) :
∫ x in A, ∫ y, f y ∂traj κ b x ∂partialTraj κ a b x₀ = ∫ y in frestrictLe b ⁻¹' A, f y ∂traj κ a x₀ :=
by
refine setIntegral_traj_partialTraj' hab ?_ hA
rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
exact hf.comp_measurable measurable_snd
