English
If i ∈ s, then the marginal value remains unchanged under a coordinate update, expressed in the congruence form: lmarginal μ s f (update x i y) = lmarginal μ s f x.
Русский
Если i ∈ s, маргинал при обновлении координаты равен исходному маргиналу.
LaTeX
$$$i \\in s \\Rightarrow (\\mathrm{lmarginal}_{μ} s f)(\\mathrm{update}\;x\;i\;y) = (\\mathrm{lmarginal}_{μ} s f)(x)$$$
Lean4
/-- Peel off a single integral from a `lmarginal` integral at the beginning (compare with
`lmarginal_erase'`, which peels off an integral at the end). -/
theorem lmarginal_erase (f : (∀ i, X i) → ℝ≥0∞) (hf : Measurable f) {i : δ} (hi : i ∈ s) (x : ∀ i, X i) :
(∫⋯∫⁻_s, f ∂μ) x = ∫⁻ xᵢ, (∫⋯∫⁻_(erase s i), f ∂μ) (Function.update x i xᵢ) ∂μ i := by
simpa [insert_erase hi] using lmarginal_insert _ hf (notMem_erase i s) x
