lmarginalPartialTraj_le — Mathlib

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

Похожие утверждения