A globally injective linearly retractive envelope

The retractive dual-evaluation coordinate supplies the linear projection and all selected exact distances. The collapsed-quotient Kuratowski coordinate separates the remaining pairs without changing those metric estimates.

@[reducible, inline]

abbrev ScottishBook155.ProtectedEnvelopeAmbient (P : Type u) (N : Type v) [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : Type (max (max v u) u)

The ambient product carrying the retractive and quotient-Kuratowski coordinates.

Equations

• ScottishBook155.ProtectedEnvelopeAmbient P N j = (ScottishBook155.RetractiveEnvelope P N j × ↥(lp (fun (x : ScottishBook155.CollapsedQuotient P (Set.range j)) => ℝ) ⊤))

noncomputable def ScottishBook155.protectedEnvelopeGenerator {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (z : N × P) : ProtectedEnvelopeAmbient P N j

A generating point with an arbitrary old-target coordinate. Allowing the first coordinate to vary independently ensures that every retractive metric embedding lands in the same closed linear span.

Equations

• ScottishBook155.protectedEnvelopeGenerator j z = ((z.1, ScottishBook155.relativeEvaluation j z.2), ScottishBook155.quotientKuratowski (Set.range j) (j 0) z.2)

@[reducible, inline]

noncomputable abbrev ScottishBook155.ProtectedEnvelope (P : Type u) (N : Type v) [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : Submodule ℝ (ProtectedEnvelopeAmbient P N j)

The actual protected envelope is the closed linear span of the generating metric coordinates, rather than the whole ambient function space. This is the density-controlled target used in the transfinite construction.

Equations

• ScottishBook155.ProtectedEnvelope P N j = (Submodule.span ℝ (Set.range (ScottishBook155.protectedEnvelopeGenerator j))).topologicalClosure

noncomputable def ScottishBook155.protectedEnvelopeDenseMap {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : (N × P →₀ ℝ) → ↥(ProtectedEnvelope P N j)

Finite linear combinations of generators, included in the closed span.

Equations

• ScottishBook155.protectedEnvelopeDenseMap j c = ⟨(Finsupp.linearCombination ℝ (ScottishBook155.protectedEnvelopeGenerator j)) c, ⋯⟩

theorem ScottishBook155.protectedEnvelopeDenseMap_denseRange {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : DenseRange (protectedEnvelopeDenseMap j)

Finite linear combinations of generators are dense in the protected envelope.

noncomputable def ScottishBook155.protectedEnvelopeSequenceEmbedding {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : ↥(ProtectedEnvelope P N j) ↪ ℕ → N × P →₀ ℝ

The closed span embeds into sequences of finite generator combinations. This is the cardinal estimate used at active successor stages.

Equations

• ScottishBook155.protectedEnvelopeSequenceEmbedding j = ScottishBook155.DenseSequenceCardinal.sequenceEmbedding (ScottishBook155.protectedEnvelopeDenseMap j) ⋯

noncomputable def ScottishBook155.protectedEnvelopeEmbeddingAmbient {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (R : P → N) (p : P) : ProtectedEnvelopeAmbient P N j

The raw metric coordinate in the ambient product.

Equations

• ScottishBook155.protectedEnvelopeEmbeddingAmbient j R p = ScottishBook155.combinedEmbedding (ScottishBook155.retractiveEmbedding j R) (Set.range j) (j 0) p

noncomputable def ScottishBook155.protectedEnvelopeEmbedding {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (R : P → N) (p : P) : ↥(ProtectedEnvelope P N j)

The final metric embedding, based at the zero point of the old target.

Equations

• ScottishBook155.protectedEnvelopeEmbedding j R p = ⟨ScottishBook155.protectedEnvelopeEmbeddingAmbient j R p, ⋯⟩

noncomputable def ScottishBook155.protectedTargetLinearAmbient {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : N →ₗ[ℝ] ProtectedEnvelopeAmbient P N j

The raw old-target embedding in the ambient product.

Equations

• ScottishBook155.protectedTargetLinearAmbient j = { toFun := fun (n : N) => ((ScottishBook155.retractiveTargetLinear j) n, 0), map_add' := ⋯, map_smul' := ⋯ }

theorem ScottishBook155.protectedEnvelopeGenerator_target {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) : protectedEnvelopeGenerator j (n, j n) = (protectedTargetLinearAmbient j) n

noncomputable def ScottishBook155.protectedTargetLinear {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : N →ₗ[ℝ] ↥(ProtectedEnvelope P N j)

The old target embeds linearly into the density-controlled envelope.

Equations

• ScottishBook155.protectedTargetLinear j = { toFun := fun (n : N) => ⟨(ScottishBook155.protectedTargetLinearAmbient j) n, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem ScottishBook155.norm_protectedTargetLinear_eq {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) : ‖(protectedTargetLinear j) n‖ = ‖n‖

noncomputable def ScottishBook155.protectedTargetLinearIsometry {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : N →ₗᵢ[ℝ] ↥(ProtectedEnvelope P N j)

The old target is a linear isometric subspace of the protected envelope.

Equations

• ScottishBook155.protectedTargetLinearIsometry j = { toLinearMap := ScottishBook155.protectedTargetLinear j, norm_map' := ⋯ }

noncomputable def ScottishBook155.protectedEnvelopeProjection {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : ↥(ProtectedEnvelope P N j) →L[ℝ] N

Projection through the first two product coordinates.

Equations

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

theorem ScottishBook155.protectedEnvelopeProjection_norm_le {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (z : ↥(ProtectedEnvelope P N j)) : ‖(protectedEnvelopeProjection j) z‖ ≤ ‖z‖

theorem ScottishBook155.protectedEnvelopeProjection_target {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) : (protectedEnvelopeProjection j) ((protectedTargetLinear j) n) = n

theorem ScottishBook155.protectedEnvelopeEmbedding_target {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (R : P → N) (hR : ∀ (n : N), R (j n) = n) (n : N) : protectedEnvelopeEmbedding j R (j n) = (protectedTargetLinear j) n

theorem ScottishBook155.protectedEnvelopeProjection_embedding {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (R : P → N) (p : P) : (protectedEnvelopeProjection j) (protectedEnvelopeEmbedding j R p) = R p

theorem ScottishBook155.protectedEnvelopeEmbedding_dist_le {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (R : P → N) (hR : ∀ (p q : P), dist (R p) (R q) ≤ dist p q) (p q : P) : dist (protectedEnvelopeEmbedding j R p) (protectedEnvelopeEmbedding j R q) ≤ dist p q

The final embedding is nonexpansive.

theorem ScottishBook155.protectedEnvelopeEmbedding_dist_eq {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (R : P → N) (hR : ∀ (p q : P), dist (R p) (R q) ≤ dist p q) {p q : P} (heval : dist (relativeEvaluation j p) (relativeEvaluation j q) = dist p q) : dist (protectedEnvelopeEmbedding j R p) (protectedEnvelopeEmbedding j R q) = dist p q

Every distance retained by relative evaluation remains exact after adding the injectivity coordinate.

theorem ScottishBook155.protectedEnvelopeEmbedding_injective {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] [CompleteSpace N] (j : N → P) (hj : Isometry j) (R : P → N) (hR : ∀ (n : N), R (j n) = n) : Function.Injective (protectedEnvelopeEmbedding j R)

If the old target is complete and isometrically embedded, the final metric embedding is globally injective.