Coherent protected chains

This is the invariant carried by the transfinite recursion: protected stages, coherent forward embeddings and backward projections, and the fixed-band recovery identity between every two stages.

structure ScottishBook155.ProtectedChain {ι : Type u} [LinearOrder ι] (r L : ℝ) : Type (u + 1)

A coherent chain of protected stages with uniform recovery radius L.

• stage : ι → ProtectedStage r

  The protected source, target, and map at each index of the chain.

• sourceSystem : CoherentBiSystem fun (i : ι) => (self.stage i).source.carrier

  The coherent embeddings and retractions between the source spaces.

• targetSystem : CoherentBiSystem fun (i : ι) => (self.stage i).target.carrier

  The coherent embeddings and retractions between the target spaces.

• compatible (i j : ι) (hij : i ≤ j) (x : (self.stage i).source.carrier) : (self.stage j).map ((self.sourceSystem.embed i j hij) x) = (self.targetSystem.embed i j hij) ((self.stage i).map x)
• recovers (i j : ι) (hij : i ≤ j) (z : (self.stage j).source.carrier) : dist z ((self.sourceSystem.embed i j hij) ((self.sourceSystem.project i j hij) z)) < L → (self.targetSystem.project i j hij) ((self.stage j).map z) = (self.stage i).map ((self.sourceSystem.project i j hij) z)

theorem ScottishBook155.ProtectedChain.ext {ι : Type u} [LinearOrder ι] {r L : ℝ} {C D : ProtectedChain r L} (hstage : C.stage = D.stage) (hsource : C.sourceSystem ≍ D.sourceSystem) (htarget : C.targetSystem ≍ D.targetSystem) : C = D

Protected chains are determined by their stage family and their two bidirectional systems; the remaining fields are propositions.

@[reducible, inline]

abbrev ScottishBook155.ProtectedChain.Source {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) (i : ι) : RealBanachSpace

The source Banach space at a specified stage of the chain.

Equations

• C.Source i = (C.stage i).source

@[reducible, inline]

abbrev ScottishBook155.ProtectedChain.Target {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) (i : ι) : RealBanachSpace

The target Banach space at a specified stage of the chain.

Equations

• C.Target i = (C.stage i).target

theorem ScottishBook155.ProtectedChain.stage_nonexpansive {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (i : ι) (x y : (C.Source i).carrier) : dist ((C.stage i).map x) ((C.stage i).map y) ≤ dist x y

Every stage map in a protected chain is nonexpansive at positive protected scale.