English
If b ≤ a, integrating against partialTraj κ a b leaves the function f unchanged; i.e., lmarginalPartialTraj κ a b f = f when f depends only on coordinates up to a.
Русский
Если b ≤ a, интегрирование по partialTraj κ a b не меняет функцию; lmarginalPartialTraj κ a b f = f, когда f зависит только от координат до a.
LaTeX
$$$ lmarginalPartialTraj\,κ\,a\,b\;f = f \quad (b \le a)$$$
Lean4
/-- If `b ≤ a`, then integrating `f` against `partialTraj κ a b` does nothing. -/
theorem lmarginalPartialTraj_le (hba : b ≤ a) {f : (Π n, X n) → ℝ≥0∞} (mf : Measurable f) :
lmarginalPartialTraj κ a b f = f := by
ext x₀
rw [lmarginalPartialTraj, partialTraj_le hba, Kernel.lintegral_deterministic']
· congr with i
simp [updateFinset]
· exact mf.comp measurable_updateFinset