Gluing a countable chain of transport plans

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

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.

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.IsProbabilityMeasure (pi n)] : MeasureTheory.Measure ((n : ℕ) → X n)

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

Equations

• TauCeti.Measure.chainMeasure pi = ProbabilityTheory.Kernel.trajMeasure (pi 0).fst (TauCeti.Measure.chainKernel✝ 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.IsProbabilityMeasure (pi n)] : MeasureTheory.IsProbabilityMeasure (chainMeasure pi)

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.IsProbabilityMeasure (pi n)] (hpi : ∀ (n : ℕ), (pi n).snd = (pi (n + 1)).fst) (n : ℕ) : MeasureTheory.Measure.map (fun (x : (n : ℕ) → X n) => x n) (chainMeasure pi) = (pi n).fst

Every time marginal of chainMeasure pi is the first marginal of the corresponding consecutive plan, provided neighboring plans have matching marginals.

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.IsProbabilityMeasure (pi n)] (hpi : ∀ (n : ℕ), (pi n).snd = (pi (n + 1)).fst) (n : ℕ) : MeasureTheory.Measure.map (fun (x : (n : ℕ) → X n) => (x n, x (n + 1))) (chainMeasure pi) = pi n

Countable chain gluing. The consecutive-coordinate projection of chainMeasure pi is the prescribed plan pi n at every 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.IsProbabilityMeasure (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.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.IsProbabilityMeasure (pi n)] (N : ℕ) : MeasureTheory.IsProbabilityMeasure (prefixChainMeasure pi N)

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.IsProbabilityMeasure (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.IsProbabilityMeasure (pi n)] (hpi : ∀ (n : ℕ), (pi n).snd = (pi (n + 1)).fst) {n N : ℕ} (hn : n < N) : MeasureTheory.Measure.map (fun (x : (i : ↥(Finset.Iic N)) → X ↑i) => (x ⟨n, ⋯⟩, x ⟨n + 1, ⋯⟩)) (prefixChainMeasure pi N) = pi n

Every adjacent projection of a finite prefix of the countable path law agrees with the prescribed plan, as long as both coordinates occur in the prefix.