English
For a measurable A of trajectories up to b, the integral over traj κ b of the indicator on A times f equals the integral over frestrictLe-preimage of A with f under traj κ a.
Русский
Для измеримой области траекторий A до времени b интеграл по traj κ b от единичной функции индикатора A и f равен интегралу по frestrictLe⁻¹'(A) с f по traj κ a.
LaTeX
$$$\\int_{x \\in A} \\int_y f(y) \\, d\\operatorname{traj}_κ b x \\, d(\\partial_κ a b x_0) = \\int_{y \\in \\operatorname{frestrictLe} b^{-1}(A)} f(y) \\, d\\operatorname{traj}_κ a x_0$$$
Lean4
theorem setIntegral_traj_partialTraj' {a b : ℕ} (hab : a ≤ b) {u : (Π i : Iic a, X i)}
{f : (Π i : Iic b, X i) → (Π n : ℕ, X n) → E} (hf : Integrable f.uncurry ((partialTraj κ a b u) ⊗ₘ (traj κ b)))
{A : Set (Π i : Iic b, X i)} (hA : MeasurableSet A) :
∫ x in A, ∫ y, f x y ∂traj κ b x ∂partialTraj κ a b u =
∫ y in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂traj κ a u :=
by
rw [← integral_integral_indicator _ _ _ hA, integral_traj_partialTraj' hab]
· simp_rw [← Set.indicator_comp_right, ← integral_indicator (measurable_frestrictLe b hA)]
rfl
convert hf.indicator (hA.prod .univ)
ext ⟨x, y⟩
by_cases hx : x ∈ A <;> simp [uncurry_def, hx]
