lmarginal_mono — Mathlib

English

A symmetric variant: the marginal over s ∪ t equals the marginal over t of the marginal over s, i.e., lmarginal μ (s∪t) f = lmarginal μ t (lmarginal μ s f).

Русский

Симметричный вариант: маргинал по s∪t равен маргиналу по t от маргинала по s: lmarginal μ (s∪t) f = lmarginal μ t (lmarginal μ s f).

LaTeX

$$$\\mathrm{lmarginal}_{μ}(s\\cup t,f) = \\mathrm{lmarginal}_{μ}(t,\\mathrm{lmarginal}_{μ}(s,f))$$$

Lean4

@[gcongr]
theorem lmarginal_mono {f g : (∀ i, X i) → ℝ≥0∞} (hfg : f ≤ g) : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ := fun _ =>
  lintegral_mono fun _ => hfg _

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