English
When δ is finite, the marginal over the whole universe univ equals the full marginal w.r.t. the product measure: (lmarginal μ univ f)(x) = ∫ f(x) d(Measure.pi μ).
Русский
При конечном множествах индексов маргинал по всему универсу равен полной маргинализации по мере произведения: lmarginal μ univ f (x) = ∫ f(x) d Measure.pi μ.
LaTeX
$$$\\big(\\mathrm{lmarginal}_{μ}(\\mathrm{univ}, f)\\big)(x) = \\int⁻ x, f x \\partial \\mathrm{Measure.pi} μ$$$
Lean4
theorem lintegral_eq_of_lmarginal_eq [Fintype δ] (s : Finset δ) {f g : (∀ i, X i) → ℝ≥0∞} (hf : Measurable f)
(hg : Measurable g) (hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ) : ∫⁻ x, f x ∂Measure.pi μ = ∫⁻ x, g x ∂Measure.pi μ :=
by
rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩
· simp_rw [lintegral_of_isEmpty]
simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_eq_of_subset (Finset.subset_univ s) hf hg hfg]
