A common complete ambient space for successive GHP couplings

Glue each next coupling along the entire current carrier, form the metric inductive limit, and take its completion. Each original coupling embeds isometrically in the resulting space. This is a geometric construction; the probability measures are subsequently transported through those embeddings.

Adapted from Freezing2/Geometry/GHPChainGluing.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

theorem BGW.MetricMeasure.exists_ghpCoupling_cost_lt {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) {ε : ℝ} (hε : ghpDistance μ ν < ε) : ∃ (C : GHPCoupling X Y), C.cost μ ν < ε

An actual near-optimal coupling is supplied by the defining infimum.

structure BGW.MetricMeasure.GHPChain.Stage (A : Type u) [MetricSpace A] : Type (u + 1)

One finite stage, recording the embedding of its latest carrier.

• ambient : Type u

  The common ambient carrier at this finite gluing stage.

• metric : MetricSpace self.ambient

  The metric on the ambient carrier.

• embed : A → self.ambient

  The isometric embedding of the latest carrier into this stage.

• isom : Isometry self.embed

@[instance_reducible]

instance BGW.MetricMeasure.GHPChain.instMetricSpaceAmbient {A : Type u} [MetricSpace A] (S : Stage A) : MetricSpace S.ambient

Equations

• BGW.MetricMeasure.GHPChain.instMetricSpaceAmbient S = S.metric

noncomputable def BGW.MetricMeasure.GHPChain.stage (X : ℕ → Type u) [(n : ℕ) → MetricSpace (X n)] [∀ (n : ℕ), Nonempty (X n)] (C : (n : ℕ) → GHPCoupling (X n) (X (n + 1))) (n : ℕ) : Stage (X n)

The finite stages are glued using the given couplings, without replacing those couplings by merely unmeasured optimal realizations.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.MetricMeasure.GHPChain.exists_complete_realization (X : ℕ → Type u) [(n : ℕ) → MetricSpace (X n)] [∀ (n : ℕ), Nonempty (X n)] (C : (n : ℕ) → GHPCoupling (X n) (X (n + 1))) : ∃ (Z : Type u) (m : MetricSpace Z) (_ : CompleteSpace Z) (ι : (n : ℕ) → X n → Z), (∀ (n : ℕ), Isometry (ι n)) ∧ ∀ (n : ℕ), ∃ (j : (C n).ambient → Z), Isometry j ∧ ι n = j ∘ (C n).left ∧ ι (n + 1) = j ∘ (C n).right

Every successive coupling factors isometrically through one common complete ambient space. The factorization identifies the whole shared carrier, and will therefore preserve the pushed middle probability measure.