Theorems · Definition · measure theory

MeasureTheory.projectiveFamilyContent

{ι : Type u_1} →
  {α : ι → Type u_2} →
    {mα : (i : ι) → MeasurableSpace (α i)} →
      {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} →
        MeasureTheory.IsProjectiveMeasureFamily P →
          MeasureTheory.AddContent ENNReal (MeasureTheory.measurableCylinders α)

For P a projective family of measures, we define an additive content on the measurable cylinders, by setting projectiveFamilyContent s = P I S for s = cylinder I S, where I is a finite set of indices and S is a measurable set in Π i : I, α i.

Defined in

Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Cited by

11 results in Mathlib

Foundations

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