English
A swapped-version statement: lmarginal μ (s ∪ t) f = lmarginal μ t (lmarginal μ s f).
Русский
Перестановочная версия: lmarginal μ (s ∪ t) f = lmarginal μ t (lmarginal μ s f).
LaTeX
$$$lmarginal μ (s\\cup t) f = lmarginal μ t (lmarginal μ s f)$$$
Lean4
theorem lmarginal_image [DecidableEq δ'] {e : δ' → δ} (he : Injective e) (s : Finset δ') {f : (∀ i, X (e i)) → ℝ≥0∞}
(hf : Measurable f) (x : ∀ i, X i) : (∫⋯∫⁻_s.image e, f ∘ (· ∘' e) ∂μ) x = (∫⋯∫⁻_s, f ∂μ ∘' e) (x ∘' e) :=
by
have h : Measurable ((· ∘' e) : (∀ i, X i) → _) := measurable_pi_iff.mpr <| fun i ↦ measurable_pi_apply (e i)
induction s using Finset.induction generalizing x with
| empty => simp
| insert _ _ hi
ih =>
rw [image_insert, lmarginal_insert _ (hf.comp h) (he.mem_finset_image.not.mpr hi), lmarginal_insert _ hf hi]
simp_rw [ih, ← update_comp_eq_of_injective' x he]
