English
For a fixed a, lmarginalPartialTraj κ a (a+1) reduces to the integral over the next coordinate with respect to κ_a, i.e., the last step of the trajectory.
Русский
Для фиксированного a lmarginalPartialTraj κ a (a+1) сводится к интегралу по следующей координате относительно κ_a, т.е. к последнему шагу траектории.
LaTeX
$$$ lmarginalPartialTraj\,κ\,a\,(a+1) f x_0 = \int⁻ x: X(a+1)\, f( update x_0 _ x ) \partial κ a ( frestrictLe a x_0 ) $$$
Lean4
/-- Integrating `f` against `partialTraj κ a b x` is the same as integrating only over the variables
from `x_{a+1}` to `x_b`. -/
theorem lmarginalPartialTraj_eq_lintegral_map [∀ n, IsSFiniteKernel (κ n)] {f : (Π n, X n) → ℝ≥0∞} (mf : Measurable f)
(x₀ : Π n, X n) :
lmarginalPartialTraj κ a b f x₀ =
∫⁻ x : (Π i : Ioc a b, X i),
f (updateFinset x₀ _ x) ∂(partialTraj κ a b).map (restrict₂ Ioc_subset_Iic_self) (frestrictLe a x₀) :=
by
nth_rw 1 [lmarginalPartialTraj, partialTraj_eq_prod, lintegral_map, lintegral_id_prod]
· congrm ∫⁻ _, f (fun i ↦ ?_) ∂_
simp only [updateFinset, mem_Iic, IicProdIoc_def, frestrictLe_apply, mem_Ioc]
split_ifs <;> try rfl
all_goals cutsat
all_goals fun_prop
