lintegral_eq_lmarginal_univ — Mathlib

English

Under suitable finiteness assumptions, lmarginal over a union equals the iterated marginal in the opposite order (swap of s and t).

Русский

При удовлетворяющих условиях конечности lmarginal над объединением равен повторному маргиналу в обратном порядке (перестановка s и t).

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow Disjoint(s,t) \\Rightarrow lmarginal μ (Finset.instUnion.union s t) f = lmarginal μ s (lmarginal μ t f)$$$

Lean4

theorem lintegral_eq_lmarginal_univ [Fintype δ] {f : (∀ i, X i) → ℝ≥0∞} (x : ∀ i, X i) :
    ∫⁻ x, f x ∂Measure.pi μ = (∫⋯∫⁻_univ, f ∂μ) x := by simp

Похожие утверждения