Measures on a finite partial order are determined by their upper sets

Mathlib's MeasureTheory.Measure.ext_of_Ici says that a finite Borel measure on a second-countable linear order is determined by its values on the closed upper rays Set.Ici a. On a finite partial order no topology is needed, and neither is a total order: the ray Set.Ici a is the point a together with the strictly larger points, so downward induction along the order recovers the mass of every singleton from the masses of the rays, and a measure on a countable space with measurable singletons is determined by its singletons.

The same downward induction shows that a family of finite measures on a finite partial order, indexed by a measurable space, is measurable into the Giry σ-algebra once its evaluations on the upper rays are measurable.

The typical consumers are laws on finite lattices of finite graphs, where the mass of a ray is the probability that a random graph contains a fixed pattern, and on products of such lattices.

Main results

• MeasureTheory.Measure.ext_of_Ici_of_finite — two measures on a finite partial order with measurable singletons, the first of them finite, agree once they agree on every Set.Ici a;
• Measurable.measure_of_Ici_of_finite — a family of finite measures on such an order is measurable once each of its upper-ray evaluations is.

theorem MeasureTheory.Measure.ext_of_Ici_of_finite {α : Type u_1} [Finite α] [PartialOrder α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ ν : Measure α) [IsFiniteMeasure μ] (h : ∀ (a : α), μ (Set.Ici a) = ν (Set.Ici a)) : μ = ν

Two measures on a finite partial order with measurable singletons are equal if they agree on all closed upper rays Set.Ici a and the first is finite: the ray at a is a together with the strictly larger points, so downward induction recovers the mass of every singleton.

theorem Measurable.measure_of_Ici_of_finite {α : Type u_1} [Finite α] [PartialOrder α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_2} [MeasurableSpace β] {μ : β → MeasureTheory.Measure α} [∀ (b : β), MeasureTheory.IsFiniteMeasure (μ b)] (h : ∀ (a : α), Measurable fun (b : β) => (μ b) (Set.Ici a)) : Measurable μ

A family of finite measures on a finite partial order with measurable singletons is measurable as soon as its value on every closed upper ray Set.Ici a depends measurably on the parameter: the mass of {a} is the mass of the ray at a minus the finitely many singleton masses strictly above a, so downward induction makes every singleton evaluation measurable, and every set is a finite union of singletons.