Assembly of the protected one-point extension #
This module combines the metric adjunction, the retractive dual-evaluation coordinate, and the quotient Kuratowski coordinate. It records the source and target embeddings and the linear recovery map together with the properties used by the successor construction.
noncomputable def
ScottishBook155.protectedSourceBaseLinearIsometry
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
:
The canonical copy of the old source as the zero-height hyperplane.
Equations
- ScottishBook155.protectedSourceBaseLinearIsometry = { toLinearMap := ↑(WithLp.linearEquiv 1 ℝ (M × ℝ)).symm ∘ₗ LinearMap.inl ℝ M ℝ, norm_map' := ⋯ }
Instances For
@[reducible, inline]
noncomputable abbrev
ScottishBook155.ProtectedExtensionSpace
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
Submodule ℝ (ProtectedEnvelopeAmbient (AdjunctionSpace V a y H hattach) N (adjunctionTargetMk V a y H hattach))
The protected envelope of the metric adjunction, relative to its original target space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ScottishBook155.protectedExtensionSourceEmbedding
{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)
(x : OneSum M)
:
↥(ProtectedExtensionSpace V a y H hattach)
The map from the extended source into the protected envelope of the adjunction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ScottishBook155.protectedExtensionTargetLinear
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
The linear embedding of the original target into the protected extension space.
Equations
- ScottishBook155.protectedExtensionTargetLinear V a y H hattach = ScottishBook155.protectedTargetLinear (ScottishBook155.adjunctionTargetMk V a y H hattach)
Instances For
noncomputable def
ScottishBook155.protectedExtensionProjection
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
The continuous linear projection from the protected extension back to the original target.
Equations
- ScottishBook155.protectedExtensionProjection V a y H hattach = ScottishBook155.protectedEnvelopeProjection (ScottishBook155.adjunctionTargetMk V a y H hattach)
Instances For
theorem
ScottishBook155.protectedExtensionTargetLinear_norm
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(n : N)
:
noncomputable def
ScottishBook155.protectedExtensionTargetLinearIsometry
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
The assembled old-target map is a linear isometric embedding.
Equations
- ScottishBook155.protectedExtensionTargetLinearIsometry V a y H hattach = { toLinearMap := ScottishBook155.protectedExtensionTargetLinear V a y H hattach, norm_map' := ⋯ }
Instances For
theorem
ScottishBook155.protectedExtensionProjection_norm_le
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(z : ↥(ProtectedExtensionSpace V a y H hattach))
:
theorem
ScottishBook155.protectedExtensionProjection_target
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(n : N)
:
(protectedExtensionProjection V a y H hattach) ((protectedExtensionTargetLinear V a y H hattach) n) = n
theorem
ScottishBook155.protectedExtensionSourceEmbedding_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)
(x z : OneSum M)
:
dist (protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap x)
(protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap z) ≤ dist x z
theorem
ScottishBook155.protectedExtensionSourceEmbedding_injective
{M : Type u}
{N : Type v}
[NormedAddCommGroup M]
[NormedAddCommGroup N]
[NormedSpace ℝ N]
[CompleteSpace 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)
(hinj : Function.Injective V)
(hy : y ∉ Set.range V)
:
Function.Injective (protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap)
theorem
ScottishBook155.protectedExtensionSourceEmbedding_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)
:
dist (protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap (WithLp.toLp 1 (m₀, s₀)))
(protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap (WithLp.toLp 1 (m₁, s₁))) = dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁))
The assembled embedding preserves every protected short source distance.
theorem
ScottishBook155.protectedExtensionSourceEmbedding_preservesUpTo
{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)
:
PreservesUpTo r (protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap)
theorem
ScottishBook155.protectedExtensionSourceEmbedding_base
{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)
(m : M)
:
protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap (WithLp.toLp 1 (m, 0)) = (protectedExtensionTargetLinear V a y H hattach) (V m)
theorem
ScottishBook155.protectedExtensionSourceEmbedding_hits
{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)
:
protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap (WithLp.toLp 1 (a, H)) = (protectedExtensionTargetLinear V a y H hattach) y
theorem
ScottishBook155.protectedExtensionProjection_source
{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)
(x : OneSum M)
:
(protectedExtensionProjection V a y H hattach) (protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap x) = sourceRetractionOne V a y L H x
theorem
ScottishBook155.protectedExtensionProjection_source_of_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)
(m : M)
{s : ℝ}
(hs : s ≤ L)
:
(protectedExtensionProjection V a y H hattach)
(protectedExtensionSourceEmbedding V a y L H hattach hLH hL hV hgap (WithLp.toLp 1 (m, s))) = V m