Successor-stage interface for claim 14

This file packages exactly the data exported by the protected one-point extension in the form needed by the transfinite construction.

structure ScottishBook155.ProtectedStage (r : ℝ) : Type (u + 1)

A stage map with the two invariants maintained throughout the recursion.

• source : RealBanachSpace

  The source real Banach space of the protected stage.

• target : RealBanachSpace

  The target real Banach space of the protected stage.

• map : self.source.carrier → self.target.carrier

  The injective stage map that preserves distances up to the protected radius.

• injective : Function.Injective self.map
• preservesUpTo : PreservesUpTo r self.map

structure ScottishBook155.ProtectedSuccessor {r : ℝ} (S : ProtectedStage r) (L : ℝ) (y : S.target.carrier) : Type (u + 1)

The complete interface of one active successor transition.

• next : ProtectedStage r

  The protected stage produced by the active successor extension.

• height : ℝ

  The extra-coordinate height at which the successor map reaches the prescribed target point.

• sourceEquiv : OneSum S.source.carrier ≃ₗᵢ[ℝ] self.next.source.carrier

  The linear isometric identification of the successor source with the old source plus a real coordinate.

• targetEmbedding : S.target.carrier →ₗᵢ[ℝ] self.next.target.carrier

  The linear isometric embedding of the old target into the successor target.

• targetRetraction : self.next.target.carrier →L[ℝ] S.target.carrier

  The contractive continuous linear retraction onto the old target.

• compatible (m : S.source.carrier) : self.next.map (self.sourceEquiv (WithLp.toLp 1 (m, 0))) = self.targetEmbedding (S.map m)
• hits : self.next.map (self.sourceEquiv (WithLp.toLp 1 (0, self.height))) = self.targetEmbedding y
• retracts (n : S.target.carrier) : self.targetRetraction (self.targetEmbedding n) = n
• contractive (z : self.next.target.carrier) : ‖self.targetRetraction z‖ ≤ ‖z‖
• flatRecovery (m : S.source.carrier) (s : ℝ) : |s| ≤ L → self.targetRetraction (self.next.map (self.sourceEquiv (WithLp.toLp 1 (m, s)))) = S.map m

noncomputable def ScottishBook155.oneSumSourceEmbedding (M : RealBanachSpace) : M.carrier →ₗᵢ[ℝ] OneSum M.carrier

The canonical old-source embedding into an l-one successor source.

Equations

• ScottishBook155.oneSumSourceEmbedding M = ScottishBook155.protectedSourceBaseLinearIsometry

noncomputable def ScottishBook155.ProtectedSuccessor.sourceEmbedding {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) : S.source.carrier →ₗᵢ[ℝ] P.next.source.carrier

The source embedding associated to a protected successor.

Equations

• P.sourceEmbedding = P.sourceEquiv.toLinearIsometry.comp (ScottishBook155.oneSumSourceEmbedding S.source)

noncomputable def ScottishBook155.ProtectedSuccessor.sourceProjection {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) : P.next.source.carrier →L[ℝ] S.source.carrier

Projection of a protected successor source onto the old source.

Equations

• P.sourceProjection = WithLp.fstL 1 ℝ S.source.carrier ℝ ∘SL ↑↑P.sourceEquiv.symm

@[simp]

theorem ScottishBook155.ProtectedSuccessor.sourceEmbedding_apply {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) (m : S.source.carrier) : P.sourceEmbedding m = P.sourceEquiv (WithLp.toLp 1 (m, 0))

@[simp]

theorem ScottishBook155.ProtectedSuccessor.sourceProjection_apply {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) (m : S.source.carrier) (s : ℝ) : P.sourceProjection (P.sourceEquiv (WithLp.toLp 1 (m, s))) = m

theorem ScottishBook155.ProtectedSuccessor.sourceProjection_retracts {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) (m : S.source.carrier) : P.sourceProjection (P.sourceEmbedding m) = m

The source projection is a left inverse of the old-stage embedding.

theorem ScottishBook155.ProtectedSuccessor.recovers_of_dist_le {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) (z : P.next.source.carrier) (hz : dist z (P.sourceEmbedding (P.sourceProjection z)) ≤ L) : P.targetRetraction (P.next.map z) = S.map (P.sourceProjection z)

The successor retraction recovers the old stage throughout the uniform source band of radius L.

structure ScottishBook155.ProtectedTransition {r : ℝ} (S : ProtectedStage r) (L : ℝ) : Type (u + 1)

A uniform successor transition, covering both active protected extensions and idle steps.

• next : ProtectedStage r

  The protected stage produced by this successor transition.

• sourceEmbedding : S.source.carrier →ₗᵢ[ℝ] self.next.source.carrier

  The linear isometric inclusion of the old source into the next source.

• sourceProjection : self.next.source.carrier →L[ℝ] S.source.carrier

  The contractive continuous linear projection from the next source to the old source.

• targetEmbedding : S.target.carrier →ₗᵢ[ℝ] self.next.target.carrier

  The linear isometric inclusion of the old target into the next target.

• targetProjection : self.next.target.carrier →L[ℝ] S.target.carrier

  The contractive continuous linear projection from the next target to the old target.

• compatible (x : S.source.carrier) : self.next.map (self.sourceEmbedding x) = self.targetEmbedding (S.map x)
• sourceRetracts (x : S.source.carrier) : self.sourceProjection (self.sourceEmbedding x) = x
• targetRetracts (y : S.target.carrier) : self.targetProjection (self.targetEmbedding y) = y
• sourceContractive (z : self.next.source.carrier) : ‖self.sourceProjection z‖ ≤ ‖z‖
• targetContractive (z : self.next.target.carrier) : ‖self.targetProjection z‖ ≤ ‖z‖
• sourceNearest (z : self.next.source.carrier) (m : S.source.carrier) : dist z (self.sourceEmbedding (self.sourceProjection z)) ≤ dist z (self.sourceEmbedding m)
• recovers (z : self.next.source.carrier) : dist z (self.sourceEmbedding (self.sourceProjection z)) ≤ L → self.targetProjection (self.next.map z) = S.map (self.sourceProjection z)

noncomputable def ScottishBook155.ProtectedSuccessor.toTransition {r L : ℝ} {S : ProtectedStage r} {y : S.target.carrier} (P : ProtectedSuccessor S L y) : ProtectedTransition S L

An active protected successor as a uniform transition.

Equations

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

noncomputable def ScottishBook155.idleTransition {r L : ℝ} (S : ProtectedStage r) : ProtectedTransition S L

The idle successor transition.

Equations

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

noncomputable def ScottishBook155.protectedSuccessor {r L : ℝ} (hr : 0 < r) (hL : 0 < L) (S : ProtectedStage r) (y : S.target.carrier) (hy : y ∉ Set.range S.map) : ProtectedSuccessor S L y

Claim 13 supplies every active successor transition required by the claim-14 recursion.

Equations

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