Theorems · Theorem · measure theory

MeasureTheory.lmarginal_singleton

∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] (f : ((i : δ) → X i) → ENNReal) (i : δ),
  ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : X i), f (Function.update x i xᵢ) ∂μ i

Defined in

Mathlib.MeasureTheory.Integral.Marginal

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEq