The dual-evaluation model of the relative Banach envelope

The paper describes the relative Lipschitz-free envelope as a quotient of an ℓ₁-sum. For the metric estimates it is equivalent, and technically more direct, to use its dual unit ball as the coordinates of an ℓ∞ space.

An admissible functional consists of a norm-at-most-one linear functional on the old normed space together with a one-Lipschitz extension to the attached metric space. Evaluation at all such functionals gives the relative coordinate. This file establishes the boundedness and nonexpansiveness of that coordinate. McShane extension and Hahn--Banach then supply enough admissible functionals to prove that the induced linear copy of the old space is isometric.

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

A dual-unit-ball functional on N together with a one-Lipschitz extension along the distinguished map j : N → P.

• linear : N →L[ℝ] ℝ

  The continuous linear functional on the distinguished target space.

• norm_le_one : ‖self.linear‖ ≤ 1
• value : P → ℝ

  The one-Lipschitz extension of the functional to the ambient metric space.

• lipschitz : LipschitzWith 1 self.value
• agree (n : N) : self.value (j n) = self.linear n

noncomputable def ScottishBook155.relativeEvaluation {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (p : P) : ↥(lp (fun (x : RelativeFunctional P N j) => ℝ) ⊤)

Evaluation on all admissible relative functionals, normalized at j 0.

Equations

• ScottishBook155.relativeEvaluation j p = ⟨fun (φ : ScottishBook155.RelativeFunctional P N j) => φ.value p - φ.value (j 0), ⋯⟩

theorem ScottishBook155.relativeEvaluation_apply {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (p : P) (φ : RelativeFunctional P N j) : ↑(relativeEvaluation j p) φ = φ.value p - φ.value (j 0)

theorem ScottishBook155.relativeEvaluation_base {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : relativeEvaluation j (j 0) = 0

theorem ScottishBook155.relativeEvaluation_dist_le {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (p q : P) : dist (relativeEvaluation j p) (relativeEvaluation j q) ≤ dist p q

The relative evaluation coordinate is nonexpansive.

theorem ScottishBook155.relativeEvaluation_target_apply {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) (φ : RelativeFunctional P N j) : ↑(relativeEvaluation j (j n)) φ = φ.linear n

On a distinguished old-space point, evaluation is exactly the underlying linear functional.

noncomputable def ScottishBook155.relativeTargetLinear {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) : N →ₗ[ℝ] ↥(lp (fun (x : RelativeFunctional P N j) => ℝ) ⊤)

The distinguished old space maps linearly into the relative coordinate.

Equations

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

theorem ScottishBook155.relativeTargetLinear_apply {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) : (relativeTargetLinear j) n = relativeEvaluation j (j n)

theorem ScottishBook155.norm_relativeTargetLinear_le {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (n : N) : ‖(relativeTargetLinear j) n‖ ≤ ‖n‖

Every admissible functional has norm at most one, so the linear copy of the old space is contractive.

theorem ScottishBook155.exists_relativeFunctional_of_isometry {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (hj : Isometry j) (L : N →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) : ∃ (φ : RelativeFunctional P N j), φ.linear = L

A contractive linear functional on the old space admits an admissible one-Lipschitz extension whenever the distinguished map is an isometry. This is the McShane extension step in the dual model.

theorem ScottishBook155.exists_relativeFunctional_norming {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (hj : Isometry j) (n : N) : ∃ (φ : RelativeFunctional P N j), φ.linear n = ‖n‖

Hahn--Banach and McShane supply a coordinate attaining the norm of every old-space vector.

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

Under an isometric distinguished map, the old space has exactly its original norm in the relative coordinate.

noncomputable def ScottishBook155.relativeTargetLinearIsometry {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (hj : Isometry j) : N →ₗᵢ[ℝ] ↥(lp (fun (x : RelativeFunctional P N j) => ℝ) ⊤)

The old Banach space embeds linearly and isometrically into the dual evaluation model of the relative envelope.

Equations

• ScottishBook155.relativeTargetLinearIsometry j hj = { toLinearMap := ScottishBook155.relativeTargetLinear j, norm_map' := ⋯ }

theorem ScottishBook155.relativeEvaluation_target_dist_eq {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (hj : Isometry j) (n m : N) : dist (relativeEvaluation j (j n)) (relativeEvaluation j (j m)) = dist n m

theorem ScottishBook155.exists_relativeFunctional_extending {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (L : N →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (s : Set P) (seed : P → ℝ) (htargets : Set.range j ⊆ s) (hseed : LipschitzOnWith 1 seed s) (hagree : ∀ (n : N), seed (j n) = L n) : ∃ (φ : RelativeFunctional P N j), φ.linear = L ∧ Set.EqOn seed φ.value s

Extend a prescribed one-Lipschitz seed which already agrees with a contractive old-space functional on every distinguished target point. This is the reusable McShane interface for the two short-distance cases.

theorem ScottishBook155.relativeEvaluation_dist_eq_of_attains {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (p q : P) (φ : RelativeFunctional P N j) (hφ : φ.value p - φ.value q = dist p q) : dist (relativeEvaluation j p) (relativeEvaluation j q) = dist p q

A single admissible functional attaining the ambient distance gives the reverse norm inequality, hence exact distance preservation by evaluation.

theorem ScottishBook155.relativeEvaluation_dist_eq_of_lipschitzOn {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (L : N →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (s : Set P) (seed : P → ℝ) (htargets : Set.range j ⊆ s) (hseed : LipschitzOnWith 1 seed s) (hagree : ∀ (n : N), seed (j n) = L n) {p q : P} (hp : p ∈ s) (hq : q ∈ s) (hpair : seed p - seed q = dist p q) : dist (relativeEvaluation j p) (relativeEvaluation j q) = dist p q

A one-Lipschitz seed on a subset, agreeing with a contractive old-space functional and attaining the distance of two points in that subset, certifies that the relative coordinate preserves that pair's distance.

noncomputable def ScottishBook155.zeroTargetPairSeed {P : Type u} [MetricSpace P] (T : Set P) (p q : P) (c₀ c₁ : ℝ) (z : P) : ℝ

The explicit McShane formula for data which vanish on T and take the values c₀,c₁ at p,q.

Equations

• ScottishBook155.zeroTargetPairSeed T p q c₀ c₁ z = min (c₀ + dist z p) (min (c₁ + dist z q) (Metric.infDist z T))

theorem ScottishBook155.zeroTargetPairSeed_lipschitz {P : Type u} [MetricSpace P] (T : Set P) (p q : P) (c₀ c₁ : ℝ) : LipschitzWith 1 (zeroTargetPairSeed T p q c₀ c₁)

theorem ScottishBook155.zeroTargetPairSeed_of_mem {P : Type u} [MetricSpace P] {T : Set P} {p q z : P} {c₀ c₁ : ℝ} (hc₀ : |c₀| ≤ Metric.infDist p T) (hc₁ : |c₁| ≤ Metric.infDist q T) (hz : z ∈ T) : zeroTargetPairSeed T p q c₀ c₁ z = 0

theorem ScottishBook155.zeroTargetPairSeed_at_left {P : Type u} [MetricSpace P] {T : Set P} {p q : P} {c₀ c₁ : ℝ} (hc₀ : |c₀| ≤ Metric.infDist p T) (hpq : |c₀ - c₁| ≤ dist p q) : zeroTargetPairSeed T p q c₀ c₁ p = c₀

theorem ScottishBook155.zeroTargetPairSeed_at_right {P : Type u} [MetricSpace P] {T : Set P} {p q : P} {c₀ c₁ : ℝ} (hc₁ : |c₁| ≤ Metric.infDist q T) (hpq : |c₀ - c₁| ≤ dist p q) : zeroTargetPairSeed T p q c₀ c₁ q = c₁

theorem ScottishBook155.exists_signed_values {d a₀ a₁ : ℝ} (hd : 0 ≤ d) (ha₀ : 0 ≤ a₀) (ha₁ : 0 ≤ a₁) (hle : d ≤ a₀ + a₁) : ∃ (c₀ : ℝ) (c₁ : ℝ), |c₀| ≤ a₀ ∧ |c₁| ≤ a₁ ∧ c₀ - c₁ = d

If d ≤ a₀+a₁, one can choose signed endpoint values bounded by the two legs and having difference exactly d.

theorem ScottishBook155.relativeEvaluation_dist_eq_of_dist_le_infDist_add {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (p q : P) (hle : dist p q ≤ Metric.infDist p (Set.range j) + Metric.infDist q (Set.range j)) : dist (relativeEvaluation j p) (relativeEvaluation j q) = dist p q

First short-distance case from the relative-envelope proof: if the direct distance is at most the sum of the distances to the old target, a functional vanishing on the old target attains that distance.

theorem ScottishBook155.exists_norming_difference {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] (n₀ n₁ : N) : ∃ (L : N →L[ℝ] ℝ), ‖L‖ ≤ 1 ∧ L n₀ - L n₁ = ‖n₀ - n₁‖

A norming functional can be chosen for the difference of two old-space vectors.

theorem ScottishBook155.exists_vertical_signed_values (s₀ s₁ : ℝ) : ∃ (c₀ : ℝ) (c₁ : ℝ), |c₀| ≤ |s₀| ∧ |c₁| ≤ |s₁| ∧ c₀ - c₁ = |s₀ - s₁|

Signed vertical endpoint values bounded by |sᵢ| can be chosen with difference |s₀-s₁|.

theorem ScottishBook155.exists_collar_endpoint_data {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] (n₀ n₁ : N) (s₀ s₁ : ℝ) : ∃ (L : N →L[ℝ] ℝ) (c₀ : ℝ) (c₁ : ℝ), ‖L‖ ≤ 1 ∧ |c₀| ≤ |s₀| ∧ |c₁| ≤ |s₁| ∧ L n₀ + c₀ - (L n₁ + c₁) = ‖n₀ - n₁‖ + |s₀ - s₁|

The algebraic data for the collar case jointly attain the sum of the horizontal norm difference and the vertical absolute difference.

theorem ScottishBook155.exists_relativeFunctional_with_two_values {P : Type u} {N : Type v} [MetricSpace P] [NormedAddCommGroup N] [NormedSpace ℝ N] (j : N → P) (hj : Isometry j) (L : N →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : P) (b₀ b₁ : ℝ) (h₀ : ∀ (n : N), dist b₀ (L n) ≤ dist p (j n)) (h₁ : ∀ (n : N), dist b₁ (L n) ≤ dist q (j n)) (hpair : dist b₀ b₁ ≤ dist p q) : ∃ (φ : RelativeFunctional P N j), φ.linear = L ∧ φ.value p = b₀ ∧ φ.value q = b₁

Compatible values on the old target and two selected points extend to an admissible relative functional. The proof uses a possibly noninjective map from N ⊕ Bool; metric compatibility forces the prescribed values to agree at every collision.

theorem ScottishBook155.relativeEvaluation_adjunctionSource_dist_eq_of_collar {M : Type u} [NormedAddCommGroup M] [NormedSpace ℝ M] {N : Type v} [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {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)) (hr : 0 < r) (hH : 2 * r + dist (V a) y < H) (hshort : PreservesUpTo r V) (m₀ m₁ : M) {s₀ s₁ : ℝ} (hs₀ : |s₀| < r) (hs₁ : |s₁| < r) (hd : dist (WithLp.toLp 1 (m₀, s₀)) (WithLp.toLp 1 (m₁, s₁)) ≤ r) : have j := adjunctionTargetMk V a y H hattach; 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 (relativeEvaluation j p₀) (relativeEvaluation j p₁) = dist p₀ p₁

In the protected collar, the algebraic endpoint data and the exact source--target formula produce an admissible functional attaining the distance of a short source pair.

theorem ScottishBook155.relativeEvaluation_adjunctionSource_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} {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)) (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 j := adjunctionTargetMk V a y H hattach; 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 (relativeEvaluation j p₀) (relativeEvaluation j p₁) = dist p₀ p₁

The two cases combine to show that the relative evaluation coordinate preserves every protected short source distance.