English
If s and t are disjoint, then the marginal over s ∪ t equals the iterated marginal: ∫⋯∫⁻_{s∪t} f ∂μ = ∫⋯∫⁻_s ∫⋯∫⁻_t f ∂μ ∂μ.
Русский
Если s и t непересекаются, то маргинал по s∪t равен повторному маргиналу: ∫⋯∫⁻_{s∪t} f ∂μ = ∫⋯∫⁻_s ∫⋯∫⁻_t f ∂μ ∂μ.
LaTeX
$$$\\int⋯∫⁻_{s\\cup t} f ∂μ = \\int⋯∫⁻_s\\, (\\int⋯∫⁻_t f ∂μ) ∂μ$; Disjoint(s,t)$$
Lean4
theorem lmarginal_singleton (f : (∀ i, X i) → ℝ≥0∞) (i : δ) :
∫⋯∫⁻_{ i }, f ∂μ = fun x => ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i :=
by
let α : Type _ := ({ i } : Finset δ)
let e := (MeasurableEquiv.piUnique fun j : α ↦ X j).symm
ext1 x
calc
(∫⋯∫⁻_{ i }, f ∂μ) x = ∫⁻ (y : X (default : α)), f (updateFinset x { i } (e y)) ∂μ (default : α) := by
simp_rw [lmarginal,
measurePreserving_piUnique (fun j : ({ i } : Finset δ) ↦ μ j) |>.symm _ |>.lintegral_map_equiv, e, α]
_ = ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i := by simp [update_eq_updateFinset]; rfl
