English
The lmarginal of a product-measure integrates out a subset of variables to yield a function in the remaining variables.
Русский
Маржинальный интеграл по части переменных реализует интегрирование по выбранной подмножество переменных.
LaTeX
$$$\text{lmarginal } μ s f x = ∫⁻ y : ∀ i : s, X_i, f (updateFinset x s y) ∂(Measure.pi μ)$$$
Lean4
/-- Integrate `f(x₁,…,xₙ)` over all variables `xᵢ` where `i ∈ s`. Return a function in the
remaining variables (it will be constant in the `xᵢ` for `i ∈ s`).
This is the marginal distribution of all variables not in `s` when the considered measure
is the product measure. -/
def lmarginal (μ : ∀ i, Measure (X i)) (s : Finset δ) (f : (∀ i, X i) → ℝ≥0∞) (x : ∀ i, X i) : ℝ≥0∞ :=
∫⁻ y : ∀ i : s, X i, f (updateFinset x s y) ∂Measure.pi fun i : s => μ i
