Gluing a countable chain of transport plans

This file turns a sequence of finite measures on consecutive products X n × X (n + 1), with matching adjacent marginals, into a finite measure on the path space ∀ n, X n. Its projection to every consecutive pair is the prescribed measure. Probability plans give a probability path law.

The construction uses Mathlib's Ionescu--Tulcea trajectory measure. At step n, the conditional kernel of the prescribed (n, n + 1)-plan is pulled back along evaluation at the last point of the current finite trajectory. The main result is TauCeti.Measure.map_adjacent_chainMeasure.

For a chain of couplings on a fixed space, TauCeti.Measure.map_adjacent_chainMeasure_of_isCoupling packages the matching-marginal hypothesis, while TauCeti.Measure.exists_measurable_isCoupling_map_chainMeasure extracts a measurable pathwise limit when almost every trajectory is Cauchy.

The finite-prefix results project this path law to any initial segment of the supplied countable chain; see TauCeti.Measure.map_adjacent_prefixChainMeasure. This is the iteration of the two-plan gluing lemma needed by optimal transport, without rebuilding Mathlib's trajectory-measure construction.

noncomputable def TauCeti.Measure.chainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] : MeasureTheory.Measure ((n : ℕ) → X n)

The path law obtained by disintegrating and iterating a countable chain of consecutive finite plans.

Equations

• TauCeti.Measure.chainMeasure pi = ProbabilityTheory.Kernel.trajMeasure (pi 0).fst (TauCeti.Measure.chainKernel✝ pi)

instance TauCeti.Measure.chainMeasure.instIsFiniteMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] : MeasureTheory.IsFiniteMeasure (chainMeasure pi)

instance TauCeti.Measure.chainMeasure.instIsProbabilityMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] [MeasureTheory.IsProbabilityMeasure (pi 0)] : MeasureTheory.IsProbabilityMeasure (chainMeasure pi)

@[simp]

theorem TauCeti.Measure.map_eval_zero_chainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] : MeasureTheory.Measure.map (fun (x : (n : ℕ) → X n) => x 0) (chainMeasure pi) = (pi 0).fst

The initial coordinate has the first marginal of the initial plan, without any matching-marginal assumption.

@[simp]

theorem TauCeti.Measure.chainMeasure_univ {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] : (chainMeasure pi) Set.univ = (pi 0) Set.univ

The path law has the total mass of the initial plan, even if later marginals do not match.

theorem TauCeti.Measure.map_eval_chainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] (n : ℕ) (hpi : ∀ k < n, (pi k).snd = (pi (k + 1)).fst) : MeasureTheory.Measure.map (fun (x : (n : ℕ) → X n) => x n) (chainMeasure pi) = (pi n).fst

The time-n marginal is the first marginal of pi n, provided neighboring plans have matching marginals before time n.

theorem TauCeti.Measure.map_adjacent_chainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] (n : ℕ) (hpi : ∀ k < n, (pi k).snd = (pi (k + 1)).fst) : MeasureTheory.Measure.map (fun (x : (n : ℕ) → X n) => (x n, x (n + 1))) (chainMeasure pi) = pi n

Countable chain gluing. The consecutive-coordinate projection at time n is pi n, provided neighboring plans have matching marginals before time n.

noncomputable def TauCeti.Measure.prefixChainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] (N : ℕ) : MeasureTheory.Measure ((i : ↥(Finset.Iic N)) → X ↑i)

The finite trajectory law obtained by projecting chainMeasure pi to coordinates at most N.

Equations

• TauCeti.Measure.prefixChainMeasure pi N = MeasureTheory.Measure.map (Preorder.frestrictLe N) (TauCeti.Measure.chainMeasure pi)

instance TauCeti.Measure.prefixChainMeasure.instIsFiniteMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] (N : ℕ) : MeasureTheory.IsFiniteMeasure (prefixChainMeasure pi N)

instance TauCeti.Measure.prefixChainMeasure.instIsProbabilityMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] [MeasureTheory.IsProbabilityMeasure (pi 0)] (N : ℕ) : MeasureTheory.IsProbabilityMeasure (prefixChainMeasure pi N)

@[simp]

theorem TauCeti.Measure.map_frestrictLe₂_prefixChainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] {M N : ℕ} (hMN : M ≤ N) : MeasureTheory.Measure.map (Preorder.frestrictLe₂ hMN) (prefixChainMeasure pi N) = prefixChainMeasure pi M

Projecting a finite prefix further gives the corresponding shorter prefix.

theorem TauCeti.Measure.map_adjacent_prefixChainMeasure {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] [∀ (n : ℕ), Nonempty (X (n + 1))] (pi : (n : ℕ) → MeasureTheory.Measure (X n × X (n + 1))) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] {n N : ℕ} (hpi : ∀ k < n, (pi k).snd = (pi (k + 1)).fst) (hn : n < N) : MeasureTheory.Measure.map (fun (x : (i : ↥(Finset.Iic N)) → X ↑i) => (x ⟨n, ⋯⟩, x ⟨n + 1, ⋯⟩)) (prefixChainMeasure pi N) = pi n

The adjacent projection at time n of a finite prefix agrees with pi n, as long as both coordinates occur in the prefix and neighboring plans match before time n.

theorem TauCeti.Measure.map_adjacent_chainMeasure_of_isCoupling {Y : Type u} [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] {mu : ℕ → MeasureTheory.Measure Y} {pi : ℕ → MeasureTheory.Measure (Y × Y)} [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] (hpi : ∀ (n : ℕ), IsCoupling (pi n) (mu n) (mu (n + 1))) (n : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → Y) => (x n, x (n + 1))) (chainMeasure pi) = pi n

Along the countable gluing chainMeasure pi of couplings pi n of consecutive laws, the nth and (n + 1)st coordinates have joint law pi n.

theorem TauCeti.Measure.exists_measurable_isCoupling_map_chainMeasure {Y : Type u} [MeasurableSpace Y] [UniformSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] [BorelSpace Y] [CompleteSpace Y] [StandardBorelSpace Y] [Nonempty Y] {mu : ℕ → MeasureTheory.Measure Y} {pi : ℕ → MeasureTheory.Measure (Y × Y)} [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (pi n)] (hpi : ∀ (n : ℕ), IsCoupling (pi n) (mu n) (mu (n + 1))) (hcauchy : ∀ᵐ (x : ℕ → Y) ∂chainMeasure pi, CauchySeq fun (n : ℕ) => x n) : ∃ (Z : (ℕ → Y) → Y), Measurable Z ∧ (∀ᵐ (x : ℕ → Y) ∂chainMeasure pi, Filter.Tendsto (fun (n : ℕ) => x n) Filter.atTop (nhds (Z x))) ∧ ∀ (n : ℕ), IsCoupling (MeasureTheory.Measure.map (fun (x : ℕ → Y) => (x n, Z x)) (chainMeasure pi)) (mu n) (MeasureTheory.Measure.map Z (chainMeasure pi))

The pathwise limit of a glued chain. If finite couplings pi n of consecutive laws are glued by chainMeasure and almost every path is Cauchy, then some measurable Z is the almost-sure limit of the coordinates, and the joint law of the nth coordinate and Z couples mu n with the law of Z.