Theorems · Theorem · measure theory

MeasureTheory.lmarginal_update_of_notMem

∀ {δ : 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)] {i : δ}
  {f : ((i : δ) → X i) → ENNReal},
  Measurable f →
    i ∉ s →
      ∀ (x : (i : δ) → X i) (y : X i),
        (∫⋯∫⁻_s, f ∂μ) (Function.update x i y) = (∫⋯∫⁻_s, f ∘ fun x => Function.update x i y ∂μ) x

Defined in

Mathlib.MeasureTheory.Integral.Marginal

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEqMeasureTheory.SigmaFinite