English
If a ≤ b ≤ c, then composing lmarginalPartialTraj κ a b and lmarginalPartialTraj κ b c equals lmarginalPartialTraj κ a c, i.e., the marginalization is transitive in this sense.
Русский
Если a ≤ b ≤ c, то композиция lmarginalPartialTraj κ a b и lmarginalPartialTraj κ b c равна lmarginalPartialTraj κ a c, то есть маргинализация транзитивна в этом смысле.
LaTeX
$$$ lmarginalPartialTraj\,κ\,a\,b\;(lmarginalPartialTraj\,κ\,b\,c\;f) = lmarginalPartialTraj\,κ\,a\,c\;f $$$
Lean4
/-- Integrating `f` against `partialTraj κ a b` and then against `partialTraj κ b c` is the same
as integrating `f` against `partialTraj κ a c`. -/
theorem lmarginalPartialTraj_self (hab : a ≤ b) (hbc : b ≤ c) {f : (Π n, X n) → ℝ≥0∞} (hf : Measurable f) :
lmarginalPartialTraj κ a b (lmarginalPartialTraj κ b c f) = lmarginalPartialTraj κ a c f :=
by
ext x₀
obtain rfl | hab := eq_or_lt_of_le hab <;> obtain rfl | hbc := eq_or_lt_of_le hbc
· rw [lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)]
· rw [lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)]
· rw [lmarginalPartialTraj_le κ le_rfl hf]
simp_rw [lmarginalPartialTraj, frestrictLe, restrict_updateFinset,
updateFinset_updateFinset_of_subset (Iic_subset_Iic.2 hbc.le)]
rw [← lintegral_comp, partialTraj_comp_partialTraj hab.le hbc.le]
fun_prop
