English
If two full tuples x and y agree outside s (i ∉ s implies x_i = y_i), then the marginal integral over s yields the same value at x and y: (∫⋯∫⁻_s f ∂μ) x = (∫⋯∫⁻_s f ∂μ) y.
Русский
Если два полноценных кортежа x и y совпадают вне множества s (для всех i ∉ s x_i = y_i), то маргинальное интегрирование по s дает одинаковые значения: (∫⋯∫⁻_s f ∂μ) x = (∫⋯∫⁻_s f ∂μ) y.
LaTeX
$$$\\displaystyle (\\int⋯∫⁻_s f ∂μ)(x) = (\\int⋯∫⁻_s f ∂μ)(y) \\quad \\text{if } x_i = y_i \\text{ for all } i \\notin s$$$
Lean4
/-- The marginal distribution is independent of the variables in `s`. -/
theorem lmarginal_congr {x y : ∀ i, X i} (f : (∀ i, X i) → ℝ≥0∞) (h : ∀ i ∉ s, x i = y i) :
(∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y := by dsimp [lmarginal, updateFinset_def]; rcongr; exact h _ ‹_›
