English
Marginal over a singleton {i} reduces to integrating only with respect to μ_i, i.e., (lmarginal μ {i} f) x = ∫⁻ x_i, f(update x i x_i) ∂μ_i.
Русский
Маргинал по одинарному множеству {i} сводится к интегрированию только по μ_i: (lmarginal μ {i} f) x = ∫⁻ x_i, f(update x i x_i) ∂μ_i.
LaTeX
$$$(\\mathrm{lmarginal}_{μ}(\\{i\\},f))(x) = \\int⁻ x_i, f(\\mathrm{update}\,x\,i\,x_i) ∂μ_i$$$
Lean4
theorem lmarginal_union (f : (∀ i, X i) → ℝ≥0∞) (hf : Measurable f) (hst : Disjoint s t) :
∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ := by
ext1 x
let e := MeasurableEquiv.piFinsetUnion X hst
calc
(∫⋯∫⁻_s ∪ t, f ∂μ) x = ∫⁻ (y : (i : ↥(s ∪ t)) → X i), f (updateFinset x (s ∪ t) y) ∂.pi fun i' : ↥(s ∪ t) ↦ μ i' :=
rfl
_ =
∫⁻ (y : ((i : s) → X i) × ((j : t) → X j)),
f (updateFinset x (s ∪ t) _) ∂(Measure.pi fun i : s ↦ μ i).prod (.pi fun j : t ↦ μ j) :=
by rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]
_ =
∫⁻ (y : (i : s) → X i),
∫⁻ (z : (j : t) → X j), f (updateFinset x (s ∪ t) (e (y, z))) ∂.pi fun j : t ↦ μ j ∂.pi fun i : s ↦ μ i :=
by
apply lintegral_prod
apply Measurable.aemeasurable
exact hf.comp <| measurable_updateFinset.comp e.measurable
_ = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x :=
by
simp_rw [lmarginal, updateFinset_updateFinset hst]
rfl
