lmarginal_le_of_subset — Mathlib

English

If s ⊆ t and f,g are measurable with same lmarginal on s, then lmarginal on t agrees for f and g as well.

Русский

Если s ⊆ t и f,g измеримы, и lmarginal по s одному и тому же значению, то lmarginal по t также совпадает для f и g.

LaTeX

$$$s \\subseteq t \\Rightarrow \\text{lmarginal}_{μ}(s,f) = \\text{lmarginal}_{μ}(s,g) \\Rightarrow \\text{lmarginal}_{μ}(t,f) = \\text{lmarginal}_{μ}(t,g)$$$

Lean4

theorem lmarginal_le_of_subset {f g : (∀ i, X i) → ℝ≥0∞} (hst : s ⊆ t) (hf : Measurable f) (hg : Measurable g)
    (hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ) : ∫⋯∫⁻_t, f ∂μ ≤ ∫⋯∫⁻_t, g ∂μ :=
  by
  rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff, lmarginal_union' μ g hg disjoint_sdiff]
  exact lmarginal_mono hfg

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