Finite measures on relational configurations

A relational configuration is a Boolean value for every atom, and configurations carry the product σ-algebra. A finite measure on configurations is therefore determined by its finite-dimensional laws, the laws of the values at finite sets of atoms. Over the vertex set ℕ, every finite set of atoms involves finitely many vertices, so a finite measure is already determined by its windows, the restrictions along Fin.val : Fin n → ℕ.

Main results

• TauCeti.RelationalConfiguration.measure_ext_of_forall_finset — a finite measure on configurations is determined by the laws of its values at finite sets of atoms;
• TauCeti.RelationalConfiguration.map_restrict_eq_of_forall_finset — the restriction of a finite measure along a vertex map is determined by the laws of the finite sets of atoms that are relabelled from the source;
• TauCeti.RelationalConfiguration.measure_ext_of_map_restrict_val — a finite measure on configurations over ℕ is determined by its windows;
• TauCeti.RelationalConfiguration.exists_map_restrict_val_eq — conversely, probability laws on the windows that are consistent under the inclusions Fin n → Fin (n + 1) are the windows of a probability law over ℕ.

The extension theorem is Kolmogorov's: the window laws prescribe the law of the values at every finite set of atoms, these laws form a projective family over the countably many atoms, and TauCeti.Measure.exists_isProjectiveLimit_of_countable realizes it. The construction follows the graph case TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Infinite.Basic, which follows C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/InfiniteLaw.lean, with the Boolean edge coordinates of a graph replaced by the Boolean atom coordinates of a configuration.

theorem TauCeti.RelationalConfiguration.measurable_restrict_eval {L : FirstOrder.Language} {V : Type u_1} (J : Finset (Atom L V)) : Measurable fun (c : RelationalConfiguration L V) => J.restrict c.eval

Reading off a finite set of atoms is measurable.

theorem TauCeti.RelationalConfiguration.measure_ext_of_forall_finset {L : FirstOrder.Language} {V : Type u_1} {μ ν : MeasureTheory.Measure (RelationalConfiguration L V)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (J : Finset (Atom L V)), MeasureTheory.Measure.map (fun (c : RelationalConfiguration L V) => J.restrict c.eval) μ = MeasureTheory.Measure.map (fun (c : RelationalConfiguration L V) => J.restrict c.eval) ν) : μ = ν

A finite measure on configurations is determined by its finite-dimensional laws, the laws of the values at finite sets of atoms.

theorem TauCeti.RelationalConfiguration.map_restrict_eq_of_forall_finset {L : FirstOrder.Language} {V : Type u_1} {W : Type u_2} {μ ν : MeasureTheory.Measure (RelationalConfiguration L W)} [MeasureTheory.IsFiniteMeasure μ] (f : V → W) (h : ∀ (J : Finset (Atom L W)), (∀ a ∈ J, ∃ (b : Atom L V), Atom.map f b = a) → MeasureTheory.Measure.map (fun (c : RelationalConfiguration L W) => J.restrict c.eval) μ = MeasureTheory.Measure.map (fun (c : RelationalConfiguration L W) => J.restrict c.eval) ν) : MeasureTheory.Measure.map (restrict f) μ = MeasureTheory.Measure.map (restrict f) ν

Two finite measures on configurations have the same restriction along a vertex map f as soon as they give the same law to every finite set of atoms relabelled along f.

theorem TauCeti.RelationalConfiguration.measure_ext_of_map_restrict_val {L : FirstOrder.Language} {μ ν : MeasureTheory.Measure (RelationalConfiguration L ℕ)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (restrict Fin.val) μ = MeasureTheory.Measure.map (restrict Fin.val) ν) : μ = ν

A finite measure on configurations over ℕ is determined by its windows, the restrictions along Fin.val : Fin n → ℕ: every finite set of atoms lies in some window, where the configuration is recovered by extending its restriction.

Extension of window laws to ℕ

theorem TauCeti.RelationalConfiguration.exists_map_restrict_val_eq {L : FirstOrder.Language} {P : (n : ℕ) → MeasureTheory.Measure (RelationalConfiguration L (Fin n))} [∀ (n : ℕ), Countable (L.Relations n)] [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (P n)] (hP : ∀ (n : ℕ), MeasureTheory.Measure.map (restrict Fin.castSucc) (P (n + 1)) = P n) : ∃ (ν : MeasureTheory.Measure (RelationalConfiguration L ℕ)), MeasureTheory.IsProbabilityMeasure ν ∧ ∀ (n : ℕ), MeasureTheory.Measure.map (restrict Fin.val) ν = P n

Kolmogorov extension for configurations over ℕ. For a language with countably many relation symbols of each arity, probability laws on the configurations on the windows Fin n that are consistent under restriction along the inclusions Fin n → Fin (n + 1) are the windows of a probability law on the configurations over ℕ. This law is unique among finite measures by measure_ext_of_map_restrict_val.