English
If f ≤ g pointwise, then marginalizing by s preserves the inequality: lmarginal_s f ≤ lmarginal_s g (pointwise).
Русский
Если f ≤ g по точкам, то маргинализация по s сохраняет неравенство: lmarginal_s f ≤ lmarginal_s g по каждому аргументу.
LaTeX
$$$f \\le g \\Rightarrow \\mathrm{lmarginal}_{\\mu}(s,f) \\le \\mathrm{lmarginal}_{\\mu}(s,g)$$$
Lean4
theorem lmarginal_update_of_mem {i : δ} (hi : i ∈ s) (f : (∀ i, X i) → ℝ≥0∞) (x : ∀ i, X i) (y : X i) :
(∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∂μ) x := by
grind [Function.update_of_ne, MeasureTheory.lmarginal_congr]