English
Equality expresses that lmarginalPartialTraj equals a Lintegral over the left-hand coordinates with a restricted partial trajectory and a map applied to the right-hand side.
Русский
Равенство выражает, что lmarginalPartialTraj равен линегралу по левым координатам с ограниченной частичной траекторией и отображением справа.
LaTeX
$$$ lmarginalPartialTraj\,κ\,a\,b\,f\ x_0 = \int⁻ x : (Π i : Ioc a b, X i) , f( updateFinset x_0 (Ioc a b) x ) ∂( partialTraj κ a b ).map (restrict₂ Ioc_subset_Iic_self) ( frestrictLe a x_0 )$$$
Lean4
@[measurability, fun_prop]
theorem measurable_lmarginalPartialTraj (a b : ℕ) {f : (Π n, X n) → ℝ≥0∞} (hf : Measurable f) :
Measurable (lmarginalPartialTraj κ a b f) :=
by
unfold lmarginalPartialTraj
let g : ((i : Iic b) → X i) × (Π n, X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 _ c.1)
let η : Kernel (Π n, X n) (Π i : Iic b, X i) := (partialTraj κ a b).comap (frestrictLe a) (measurable_frestrictLe _)
change Measurable fun x₀ ↦ ∫⁻ z : (i : Iic b) → X i, g (z, x₀) ∂η x₀
refine Measurable.lintegral_kernel_prod_left' <| hf.comp ?_
simp only [updateFinset, measurable_pi_iff]
intro i
by_cases h : i ∈ Iic b <;> simp only [h, ↓reduceDIte] <;> fun_prop
