The flat cutoff used in the protected extension

This module formalizes the scalar cutoff from the last part of lem:protected-extension. It is independent of the still-missing Lipschitz-free-space construction.

noncomputable def ScottishBook155.flatCutoff (L H s : ℝ) : ℝ

The cutoff which is zero through L, affine between L and H, and one from H onward.

Equations

• ScottishBook155.flatCutoff L H s = ↑(Set.projIcc 0 1 ScottishBook155.flatCutoff._proof_1 ((s - L) / (H - L)))

theorem ScottishBook155.flatCutoff_of_le {L H s : ℝ} (hLH : L < H) (hs : s ≤ L) : flatCutoff L H s = 0

theorem ScottishBook155.flatCutoff_of_ge {L H s : ℝ} (hLH : L < H) (hs : H ≤ s) : flatCutoff L H s = 1

theorem ScottishBook155.flatCutoff_mem_Icc (L H s : ℝ) : flatCutoff L H s ∈ Set.Icc 0 1

theorem ScottishBook155.flatCutoff_abs_sub_le {L H : ℝ} (hLH : L < H) (s t : ℝ) : |flatCutoff L H s - flatCutoff L H t| ≤ 1 / (H - L) * |s - t|

The exact Lipschitz estimate used for the flat retraction.

noncomputable def ScottishBook155.sourceRetraction {M : Type u_1} {N : Type u_2} [AddCommGroup N] [Module ℝ N] (V : M → N) (a : M) (y : N) (L H : ℝ) (m : M) (s : ℝ) : N

The nonlinear map into the old target which becomes flat on all source coordinates at most L.

Equations

• ScottishBook155.sourceRetraction V a y L H m s = V m + ScottishBook155.flatCutoff L H s • (y - V a)

theorem ScottishBook155.sourceRetraction_of_le {M : Type u_1} {N : Type u_2} [AddCommGroup N] [Module ℝ N] {V : M → N} {a m : M} {y : N} {L H s : ℝ} (hLH : L < H) (hs : s ≤ L) : sourceRetraction V a y L H m s = V m

theorem ScottishBook155.sourceRetraction_norm_sub_le {M : Type u_1} {N : Type u_2} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hV : ∀ (m n : M), ‖V m - V n‖ ≤ ‖m - n‖) (hgap : ‖y - V a‖ ≤ H - L) (m n : M) (s t : ℝ) : ‖sourceRetraction V a y L H m s - sourceRetraction V a y L H n t‖ ≤ ‖m - n‖ + |s - t|

The norm estimate proving that the source retraction is nonexpansive for the sum norm, provided the attachment gap is at most H - L.

theorem ScottishBook155.sourceRetraction_hits_attachment {M : Type u_1} {N : Type u_2} [AddCommGroup N] [Module ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) : sourceRetraction V a y L H a H = y

theorem ScottishBook155.sourceRetraction_base {M : Type u_1} {N : Type u_2} [AddCommGroup N] [Module ℝ N] {V : M → N} {a m : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) : sourceRetraction V a y L H m 0 = V m

theorem ScottishBook155.sourceRetraction_attachment {M : Type u_1} {N : Type u_2} [AddCommGroup N] [Module ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hL : 0 ≤ L) (p : M ⊕ Unit) : sourceRetraction V a y L H (WithLp.fst (attachmentPoint a H p)) (WithLp.snd (attachmentPoint a H p)) = attachmentMap V y p

The source retraction agrees with the prescribed attachment map on the whole attachment set.

theorem ScottishBook155.sourceRetraction_dist_le {M : Type u_1} {N : Type u_2} [NormedAddCommGroup M] [NormedAddCommGroup N] [NormedSpace ℝ N] {V : M → N} {a : M} {y : N} {L H : ℝ} (hLH : L < H) (hV : ∀ (m n : M), dist (V m) (V n) ≤ dist m n) (hgap : dist y (V a) ≤ H - L) (x z : OneSum M) : dist (sourceRetraction V a y L H (WithLp.fst x) (WithLp.snd x)) (sourceRetraction V a y L H (WithLp.fst z) (WithLp.snd z)) ≤ dist x z

Metric form of the source-retraction estimate on the sum-norm source.