English
If i ∈ s, erasing i from s shifts the marginal: lmarginal μ s f x equals lmarginal μ (erase s i) f applied to update x i x_i, integrated over μ_i.
Русский
Если i ∈ s, удаление i из s переносит маргинал: lmarginal μ s f x = lmarginal μ (erase s i) f (update x i x_i) интегрируется по μ_i.
LaTeX
$$$i \\in s \\Rightarrow (\\mathrm{lmarginal}_{μ} s f)(x) = (\\int⁻ x_i, (\\mathrm{lmarginal}_{μ}(s\\setminus\\{i\\}) f)(\\mathrm{update}\;x\;i\;x_i) ∂μ_i)$$$
Lean4
/-- Peel off a single integral from a `lmarginal` integral at the end (compare with
`lmarginal_insert`, which peels off an integral at the beginning). -/
theorem lmarginal_insert' (f : (∀ i, X i) → ℝ≥0∞) (hf : Measurable f) {i : δ} (hi : i ∉ s) :
∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i) ∂μ := by
rw [Finset.insert_eq, Finset.union_comm, lmarginal_union (s := s) μ f hf (Finset.disjoint_singleton_right.mpr hi),
lmarginal_singleton]
