Theorems · Theorem · measure theory

MeasureTheory.lmarginal_insert

∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f →
    ∀ {i : δ},
      i ∉ s →
        ∀ (x : (i : δ) → X i), (∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : X i), (∫⋯∫⁻_s, f ∂μ) (Function.update x i xᵢ) ∂μ i

Peel off a single integral from a lmarginal integral at the beginning (compare with lmarginal_insert', which peels off an integral at the end).

Defined in

Mathlib.MeasureTheory.Integral.Marginal

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEqMeasureTheory.SigmaFinite