Theorems · Definition · measure theory

MeasureTheory.lmarginal

{δ : Type u_1} →
  {X : δ → Type u_3} →
    [inst : (i : δ) → MeasurableSpace (X i)] →
      [DecidableEq δ] →
        ((i : δ) → MeasureTheory.Measure (X i)) → Finset δ → (((i : δ) → X i) → ENNReal) → ((i : δ) → X i) → ENNReal

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.

Defined in

Mathlib.MeasureTheory.Integral.Marginal

Cited by

28 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceDecidableEq