A retractive dual-evaluation envelope

The dual-evaluation coordinate already gives the metric part of the relative envelope. Adjoining the old target as a max-product coordinate makes the retraction linear and explicit: it is first-coordinate projection.

@[reducible, inline]

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

The old target together with the dual-evaluation relative coordinate.

Equations

• ScottishBook155.RetractiveEnvelope P N j = (N × ↥(lp (fun (x : ScottishBook155.RelativeFunctional P N j) => ℝ) ⊤))

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

Embed the attached metric space using a chosen metric retraction and the relative evaluation coordinate.

Equations

• ScottishBook155.retractiveEmbedding j R p = (R p, ScottishBook155.relativeEvaluation j p)

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

The old target embeds linearly in both coordinates.

Equations

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

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

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

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

Equations

• ScottishBook155.retractiveTargetLinearIsometry j = { toLinearMap := ScottishBook155.retractiveTargetLinear j, norm_map' := ⋯ }

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

First-coordinate projection is the contractive linear retraction.

Equations

• ScottishBook155.retractiveProjection j = ContinuousLinearMap.fst ℝ N ↥(lp (fun (x : ScottishBook155.RelativeFunctional P N j) => ℝ) ⊤)

theorem ScottishBook155.retractiveProjection_target {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) : (retractiveProjection j) ((retractiveTargetLinear j) n) = n

theorem ScottishBook155.retractiveProjection_norm_le {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (z : RetractiveEnvelope P N j) : ‖(retractiveProjection j) z‖ ≤ ‖z‖

theorem ScottishBook155.retractiveEmbedding_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) : retractiveEmbedding j R (j n) = (retractiveTargetLinear j) n

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

theorem ScottishBook155.retractiveEmbedding_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 (retractiveEmbedding j R p) (retractiveEmbedding j R q) ≤ dist p q

A nonexpansive metric retraction and relative evaluation jointly give a nonexpansive embedding into the max-product envelope.

theorem ScottishBook155.retractiveEmbedding_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 (retractiveEmbedding j R p) (retractiveEmbedding j R q) = dist p q

Every distance retained by relative evaluation remains exact in the retractive envelope.