The adjunction inside a linearly retractive Banach envelope

This file specializes the retractive dual-evaluation envelope to the metric adjunction. The resulting metric embedding is nonexpansive, retains all protected short source distances, extends the linear isometric copy of the old target, and recovers the nonlinear adjunction retraction by a contractive linear projection.

noncomputable def ScottishBook155.adjunctionEnvelopeEmbedding {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (p : AdjunctionSpace V a y H hattach) : RetractiveEnvelope (AdjunctionSpace V a y H hattach) N (adjunctionTargetMk V a y H hattach)

The retractive-envelope embedding of the adjunction space, using its canonical target inclusion and retraction.

Equations

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

theorem ScottishBook155.adjunctionEnvelopeEmbedding_target {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (n : N) : adjunctionEnvelopeEmbedding V a y L H hattach hLH hL hV hgap (adjunctionTargetMk V a y H hattach n) = (retractiveTargetLinear (adjunctionTargetMk V a y H hattach)) n

theorem ScottishBook155.adjunctionEnvelopeEmbedding_dist_le {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (p q : AdjunctionSpace V a y H hattach) : dist (adjunctionEnvelopeEmbedding V a y L H hattach hLH hL hV hgap p) (adjunctionEnvelopeEmbedding V a y L H hattach hLH hL hV hgap q) ≤ dist p q

theorem ScottishBook155.adjunctionEnvelopeProjection_recovery {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (p : AdjunctionSpace V a y H hattach) : (retractiveProjection (adjunctionTargetMk V a y H hattach)) (adjunctionEnvelopeEmbedding V a y L H hattach hLH hL hV hgap p) = adjunctionRetraction V a y L H hattach hLH hL hV hgap p

theorem ScottishBook155.adjunctionEnvelopeEmbedding_source_dist_eq_of_short {M : Type u} [NormedAddCommGroup M] [NormedSpace ℝ M] {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H r : ℝ} (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q)) (hLH : L < H) (hL : 0 ≤ L) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (hr : 0 < r) (hH : 2 * r + dist (V a) y < H) (hshort : PreservesUpTo r V) (m₀ m₁ : M) {s₀ s₁ : ℝ} (hd : dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁)) ≤ r) : have p₀ := adjunctionSourceMk V a y H hattach (WithLp.toLp 1 (m₀, s₀)); have p₁ := adjunctionSourceMk V a y H hattach (WithLp.toLp 1 (m₁, s₁)); dist (adjunctionEnvelopeEmbedding V a y L H hattach hLH hL hV hgap p₀) (adjunctionEnvelopeEmbedding V a y L H hattach hLH hL hV hgap p₁) = dist p₀ p₁

The retractive envelope retains every protected short source distance.