English
If i ∈ s, then updating the i-th coordinate of x leaves the marginal unchanged: lmarginal μ s f (update x i y) = lmarginal μ s f x.
Русский
Если i принадлежит s, то замена i-й координаты x на y не меняет маргинал: lmarginal μ s f (update x i y) = lmarginal μ s f x.
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_insert'`, which peels off an integral at the end). -/
theorem lmarginal_insert (f : (∀ i, X i) → ℝ≥0∞) (hf : Measurable f) {i : δ} (hi : i ∉ s) (x : ∀ i, X i) :
(∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ xᵢ, (∫⋯∫⁻_s, f ∂μ) (Function.update x i xᵢ) ∂μ i := by
rw [Finset.insert_eq, lmarginal_union μ f hf (Finset.disjoint_singleton_left.mpr hi), lmarginal_singleton]
