A product law is determined by finite-dimensional marginals in its path coordinate

A finite measure on γ × (∀ i, β i) is determined by its images under Prod.map id F.restrict, as F ranges over the finite sets of coordinates. On a rectangle s ×ˢ t, the section t ↦ μ (s ×ˢ t) is a finite measure on the path space ∀ i, β i, which is the projective limit of its finite-dimensional marginals and hence determined by them; rectangles in turn determine a finite measure on a product.

This is the shape in which a coding of an infinite family of random variables, jointly with a fixed observation, is assembled from the codings of its finite subfamilies. The argument is the one that closes TauCeti.Probability.SeparatelyExchangeable.exists_common_visibleArray_coding (in TauCeti.Probability.Exchangeability.Arrays.Strip.Cell.CommonCoding), stated here for an arbitrary observation space and path space.

Main result

• TauCeti.MeasureTheory.Measure.ext_prod_pi_of_forall_finset_map_restrict_eq — two finite measures on γ × (∀ i, β i) with the same image under every Prod.map id F.restrict are equal.

theorem TauCeti.MeasureTheory.Measure.ext_prod_pi_of_forall_finset_map_restrict_eq {γ : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [MeasurableSpace γ] [(i : ι) → MeasurableSpace (β i)] {μ ν : MeasureTheory.Measure (γ × ((i : ι) → β i))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (F : Finset ι), MeasureTheory.Measure.map (Prod.map id F.restrict) μ = MeasureTheory.Measure.map (Prod.map id F.restrict) ν) : μ = ν

Finite-dimensional marginals in the path coordinate determine a finite product law. Two finite measures on γ × (∀ i, β i) are equal as soon as, for every finite set F of coordinates, their images under Prod.map id F.restrict agree.