English
If f depends only on variables up to a and a ≤ c ≤ d, then lmarginalPartialTraj κ b c f = lmarginalPartialTraj κ b d f; the right-hand truncation does not affect the value.
Русский
Если f зависит только от переменных до a и a ≤ c ≤ d, то lmarginalPartialTraj κ b c f = lmarginalPartialTraj κ b d f; правая обрезка не влияет на значение.
LaTeX
$$$ lmarginalPartialTraj\,κ\,b\,c\;f = lmarginalPartialTraj\,κ\,b\,d\;f $$$
Lean4
/-- If `f` only depends on the variables uo to rank `a`, integrating beyond rank `a` is the same
as integrating up to rank `a`. -/
theorem lmarginalPartialTraj_const_right [∀ n, IsMarkovKernel (κ n)] {d : ℕ} {f : (Π n, X n) → ℝ≥0∞} (mf : Measurable f)
(hf : DependsOn f (Iic a)) (hac : a ≤ c) (had : a ≤ d) :
lmarginalPartialTraj κ b c f = lmarginalPartialTraj κ b d f :=
by
wlog hcd : c ≤ d generalizing c d
· rw [this had hac (le_of_not_ge hcd)]
obtain hbc | hcb := le_total b c
· rw [← lmarginalPartialTraj_self hbc hcd mf, hf.lmarginalPartialTraj_of_le d mf hac]
· rw [hf.lmarginalPartialTraj_of_le c mf (hac.trans hcb), hf.lmarginalPartialTraj_of_le d mf (hac.trans hcb)]
