English
For a function f of two trajectory indices, integrating over traj at b and partialTraj yields equal to integrating the uncurried f over the traj at a after applying frestrictLe.
Русский
Для функции двух индексов траекторий интегрирование по traj в точке b и partialTraj дает то же самое, что интегрирование по нечистенной функции f по traj a после применения frestrictLe.
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 : (Π i : Iic b, X i) → (Π n : ℕ, X n) → E} (hf : Integrable f.uncurry ((partialTraj κ a b x₀) ⊗ₘ (traj κ b))) :
∫ x, ∫ y, f x y ∂traj κ b x ∂partialTraj κ a b x₀ = ∫ x, f (frestrictLe b x) x ∂traj κ a x₀ :=
by
have hf' := hf
rw [partialTraj_compProd_traj hab] at hf'
simp_rw [← uncurry_apply_pair f, ← Measure.integral_compProd hf, partialTraj_compProd_traj hab,
integral_map (by fun_prop) hf'.1]
