lmarginal_update_of_mem — Mathlib

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]

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