English
If i ∈ s, removing i from s in lmarginal μ s f equals lmarginal μ (erase s i) of a corresponding transformed f.
Русский
Если i ∈ s, удаление i из s в lmarginal μ s f эквивалентно lmarginal μ (erase s i) от трансформированного f.
LaTeX
$$$i \\in s \\Rightarrow (\\mathrm{lmarginal}_{μ} s f) = (\\mathrm{lmarginal}_{μ} (erase s i) (f\\circ' (update \\,·\, i \\,\\cdot)))$$$
Lean4
/-- Peel off a single integral from a `lmarginal` integral at the end (compare with
`lmarginal_erase`, which peels off an integral at the beginning). -/
theorem lmarginal_erase' (f : (∀ i, X i) → ℝ≥0∞) (hf : Measurable f) {i : δ} (hi : i ∈ s) :
∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_(erase s i), (fun x ↦ ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i) ∂μ := by
simpa [insert_erase hi] using lmarginal_insert' _ hf (notMem_erase i s)
