Existence form of the protected one-point extension

The preceding files construct the extension from a height satisfying explicit inequalities. Here the height is chosen and the resulting properties are packaged in the hypothesis form of the manuscript's protected-extension lemma.

noncomputable def ScottishBook155.protectedHeight {M : Type u} {N : Type v} [Zero M] [PseudoMetricSpace N] (V : M → N) (y : N) (L r : ℝ) : ℝ

A concrete height leaving room for the attachment gap, the recovery collar, and the protected metric scale.

Equations

• ScottishBook155.protectedHeight V y L r = dist (V 0) y + L + 4 * r

theorem ScottishBook155.protectedHeight_L_lt {M : Type u} {N : Type v} [Zero M] [PseudoMetricSpace N] {V : M → N} {y : N} {L r : ℝ} (_hL : 0 < L) (hr : 0 < r) : L < protectedHeight V y L r

theorem ScottishBook155.protectedHeight_attachment_gap {M : Type u} {N : Type v} [Zero M] [PseudoMetricSpace N] {V : M → N} {y : N} {L r : ℝ} (hL : 0 < L) (hr : 0 < r) : dist (V 0) y < protectedHeight V y L r

theorem ScottishBook155.protectedHeight_retraction_gap {M : Type u} {N : Type v} [Zero M] [PseudoMetricSpace N] {V : M → N} {y : N} {L r : ℝ} (hr : 0 < r) : dist y (V 0) ≤ protectedHeight V y L r - L

theorem ScottishBook155.protectedHeight_short_gap {M : Type u} {N : Type v} [Zero M] [PseudoMetricSpace N] {V : M → N} {y : N} {L r : ℝ} (hL : 0 < L) (hr : 0 < r) : 2 * r + dist (V 0) y < protectedHeight V y L r

theorem ScottishBook155.exists_protectedExtension {M : Type u} {N : Type v} [NormedAddCommGroup M] [NormedSpace ℝ M] [NormedAddCommGroup N] [NormedSpace ℝ N] [CompleteSpace N] {V : M → N} {y : N} {L r : ℝ} (hL : 0 < L) (hr : 0 < r) (hinj : Function.Injective V) (hshort : PreservesUpTo r V) (hy : y ∉ Set.range V) : ∃ (H : ℝ) (hattach : ∀ (p q : M ⊕ Unit), dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint 0 H p) (attachmentPoint 0 H q)) (hLH : L < H) (hgap : dist y (V 0) ≤ H - L), Function.Injective (protectedExtensionSourceEmbedding V 0 y L H hattach hLH ⋯ ⋯ hgap) ∧ PreservesUpTo r (protectedExtensionSourceEmbedding V 0 y L H hattach hLH ⋯ ⋯ hgap) ∧ (∀ (m : M), protectedExtensionSourceEmbedding V 0 y L H hattach hLH ⋯ ⋯ hgap (WithLp.toLp 1 (m, 0)) = (protectedExtensionTargetLinear V 0 y H hattach) (V m)) ∧ protectedExtensionSourceEmbedding V 0 y L H hattach hLH ⋯ ⋯ hgap (WithLp.toLp 1 (0, H)) = (protectedExtensionTargetLinear V 0 y H hattach) y ∧ (∀ (n : N), ‖(protectedExtensionTargetLinear V 0 y H hattach) n‖ = ‖n‖) ∧ (∀ (z : ↥(ProtectedExtensionSpace V 0 y H hattach)), ‖(protectedExtensionProjection V 0 y H hattach) z‖ ≤ ‖z‖) ∧ (∀ (n : N), (protectedExtensionProjection V 0 y H hattach) ((protectedExtensionTargetLinear V 0 y H hattach) n) = n) ∧ ∀ (m : M) (s : ℝ), |s| ≤ L → (protectedExtensionProjection V 0 y H hattach) (protectedExtensionSourceEmbedding V 0 y L H hattach hLH ⋯ ⋯ hgap (WithLp.toLp 1 (m, s))) = V m

The complete protected-extension package: a concrete Banach target and maps satisfying local isometry, injectivity, extension, point-hitting, linear retraction, and collar recovery.