Coherent retractions on a completed normed direct limit

This file formalizes the linear part of the recovery mechanism at a limit stage. A coherent family of contractive projections to an earlier component extends to a contractive linear map from the completed direct limit.

theorem ScottishBook155.CoherentRetractionLimit.linearDirectedSystem {ι : Type u} [LinearOrder ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] : DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(NormedDirectLimit.linearMap N e x1 x2 x3)

structure ScottishBook155.CoherentRetractionLimit.ProjectionFamily {ι : Type u} [LinearOrder ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) (a : ι) : Type u

A projection to a fixed earlier component, defined coherently on every component of the directed system.

• project (i : ι) : N i →L[ℝ] N a

  Coherent contractive projections from each component onto the fixed component indexed by a.

• coherent (i j : ι) (hij : i ≤ j) (x : N i) : (self.project j) ((e i j hij) x) = (self.project i) x
• contractive (i : ι) (x : N i) : ‖(self.project i) x‖ ≤ ‖x‖
• leftInverse (x : N a) : (self.project a) x = x

noncomputable def ScottishBook155.CoherentRetractionLimit.ProjectionFamily.completedProjection {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] {a : ι} (P : ProjectionFamily N e a) : NormedDirectLimit.CompletedCarrier N e →L[ℝ] N a

The projection family induces a contractive linear map from the completed direct limit.

Equations

• ScottishBook155.CoherentRetractionLimit.ProjectionFamily.completedProjection N e P = ScottishBook155.NormedDirectLimit.completedLift N e P.project ⋯ 1 ⋯

theorem ScottishBook155.CoherentRetractionLimit.ProjectionFamily.completedProjection_completedOf {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] {a : ι} (P : ProjectionFamily N e a) (i : ι) (x : N i) : (completedProjection N e P) ((NormedDirectLimit.completedOf N e i) x) = (P.project i) x

theorem ScottishBook155.CoherentRetractionLimit.ProjectionFamily.completedProjection_retracts {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] {a : ι} (P : ProjectionFamily N e a) (x : N a) : (completedProjection N e P) ((NormedDirectLimit.completedOf N e a) x) = x

The completed projection retracts the canonical copy of its chosen component.

theorem ScottishBook155.CoherentRetractionLimit.ProjectionFamily.completedProjection_norm_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] {a : ι} (P : ProjectionFamily N e a) (z : NormedDirectLimit.CompletedCarrier N e) : ‖(completedProjection N e P) z‖ ≤ ‖z‖

The completed projection is contractive.

structure ScottishBook155.CoherentRetractionLimit.ProjectionSystem {ι : Type u} [LinearOrder ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) : Type u

Coherent projections to every component of the directed system. Below the projection index they are the forward embeddings; above it they are the specified retractions.

• project (a i : ι) : N i →L[ℝ] N a

  Coherent contractive maps between components, equal to forward embeddings below the target index.

• coherent (a i j : ι) (hij : i ≤ j) (x : N i) : (self.project a j) ((e i j hij) x) = (self.project a i) x
• contractive (a i : ι) (x : N i) : ‖(self.project a i) x‖ ≤ ‖x‖
• identityBelow (i a : ι) (hia : i ≤ a) (x : N i) : (self.project a i) x = (e i a hia) x

noncomputable def ScottishBook155.CoherentRetractionLimit.ProjectionSystem.family {ι : Type u} [LinearOrder ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) (a : ι) : ProjectionFamily N e a

The projection system restricted to one fixed component.

Equations

• ScottishBook155.CoherentRetractionLimit.ProjectionSystem.family N e P a = { project := P.project a, coherent := ⋯, contractive := ⋯, leftInverse := ⋯ }

noncomputable def ScottishBook155.CoherentRetractionLimit.ProjectionSystem.approx {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) (a : ι) (z : NormedDirectLimit.CompletedCarrier N e) : NormedDirectLimit.CompletedCarrier N e

Project a completed-limit vector to component a and include it back into the completed limit.

Equations

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

theorem ScottishBook155.CoherentRetractionLimit.ProjectionSystem.approx_completedOf_of_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) {i a : ι} (hia : i ≤ a) (x : N i) : approx N e P a ((NormedDirectLimit.completedOf N e i) x) = (NormedDirectLimit.completedOf N e i) x

Once a lies above a component, approximation fixes that entire component pointwise.

theorem ScottishBook155.CoherentRetractionLimit.ProjectionSystem.approx_dist_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) (a : ι) (z w : NormedDirectLimit.CompletedCarrier N e) : dist (approx N e P a z) (approx N e P a w) ≤ dist z w

Every approximation map is nonexpansive.

theorem ScottishBook155.CoherentRetractionLimit.ProjectionSystem.approx_tendsto {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) (z : NormedDirectLimit.CompletedCarrier N e) : Filter.Tendsto (fun (a : ι) => approx N e P a z) Filter.atTop (nhds z)

Coherent contractive projections converge strongly to the identity on the completed direct limit.

theorem ScottishBook155.CoherentRetractionLimit.ProjectionSystem.eventually_dist_approx_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) {L : ℝ} (hL : 0 < L) (z : NormedDirectLimit.CompletedCarrier N e) : ∀ᶠ (a : ι) in Filter.atTop, dist z (approx N e P a z) ≤ L

For a positive recovery band, every completed-limit vector eventually lies within that band of its projected approximation.

theorem ScottishBook155.CoherentRetractionLimit.ProjectionSystem.eventually_dist_approx_lt {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (e : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(e x1 x2 x3)] (P : ProjectionSystem N e) {L : ℝ} (hL : 0 < L) (z : NormedDirectLimit.CompletedCarrier N e) : ∀ᶠ (a : ι) in Filter.atTop, dist z (approx N e P a z) < L

Strict form of eventual approximation, used when the recovery invariant is stated on an open band.