lmarginalPartialTraj_mono — Mathlib

English

Equates lmarginalPartialTraj with a Lintegral of a function against the restricted partial trajectory, making the dependence on left variables explicit.

Русский

Сопоставляет lmarginalPartialTraj с линегралом функции против ограниченной частичной траектории, делая зависимость от левых переменных явной.

LaTeX

$$$ lmarginalPartialTraj\,κ\,a\,b\;f\;x_0 = \int⁻ f( updateFinset\ x_0 ) d( partialTraj\ κ\ a\ b )_{restrict₂} $$$

Lean4

theorem lmarginalPartialTraj_mono (a b : ℕ) {f g : (Π n, X n) → ℝ≥0∞} (hfg : f ≤ g) (x₀ : Π n, X n) :
    lmarginalPartialTraj κ a b f x₀ ≤ lmarginalPartialTraj κ a b g x₀ :=
  lintegral_mono fun _ ↦ hfg _

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