English
Peeling off a single integral from the left of lmarginal: inserting i into s yields a decomposition into inner and outer integrals.
Русский
Отделение одного интеграла слева от lmarginal: добавление i в s дает разложение на вложенные интегралы.
LaTeX
$$$(\\int⋯∫⁻_{insert i s} f ∂μ)(x) = \\int⁻ x_i, (\\int⋯∫⁻_s f ∂μ)(update x i x_i) ∂μ_i$$$
Lean4
theorem lmarginal_update_of_notMem {i : δ} {f : (∀ i, X i) → ℝ≥0∞} (hf : Measurable f) (hi : i ∉ s) (x : ∀ i, X i)
(y : X i) : (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∘ (Function.update · i y) ∂μ) x := by
induction s using Finset.induction generalizing x with
| empty => simp
| insert i' s hi'
ih =>
rw [lmarginal_insert _ hf hi', lmarginal_insert _ (hf.comp measurable_update_left) hi']
have hii' : i ≠ i' := mt (by rintro rfl; exact mem_insert_self i s) hi
simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]
