Protected stages from completed directed limits

This file combines the completed nonlinear limit map with coherent source and target projections. Contractive source projections prove short-distance preservation; eventual target recovery and injectivity of the earlier stages prove injectivity of the completed map.

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

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

@[reducible, inline]

abbrev ScottishBook155.DirectedLimitStage.Source {ι : Type u} [LinearOrder ι] [Nonempty ι] (M : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] : Type u

The completed direct limit of the source stages.

Equations

• ScottishBook155.DirectedLimitStage.Source M eM = ScottishBook155.NormedDirectLimit.CompletedCarrier M eM

@[reducible, inline]

abbrev ScottishBook155.DirectedLimitStage.Target {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] : Type u

The completed direct limit of the target stages.

Equations

• ScottishBook155.DirectedLimitStage.Target N eN = ScottishBook155.NormedDirectLimit.CompletedCarrier N eN

noncomputable def ScottishBook155.DirectedLimitStage.limitMap {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) : Source M eM → Target N eN

The continuous extension to completed limits of the compatible nonexpansive stage maps.

Equations

• ScottishBook155.DirectedLimitStage.limitMap M N eM eN V = ScottishBook155.CompletedLimitMap.completedMap M N eM eN V

theorem ScottishBook155.DirectedLimitStage.limitMap_preservesUpTo {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) {r : ℝ} (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (stagePreserves : ∀ (i : ι), PreservesUpTo r (V i)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) : PreservesUpTo r (limitMap M N eM eN V)

The completed limit map preserves the protected scale whenever every earlier stage does.

theorem ScottishBook155.DirectedLimitStage.limitMap_injective {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (targetProjection : CoherentRetractionLimit.ProjectionSystem N eN) (stageInjective : ∀ (i : ι), Function.Injective (V i)) (eventualRecovery : ∀ (x : Source M eM), ∀ᶠ (a : ι) in Filter.atTop, (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)) : Function.Injective (limitMap M N eM eN V)

Eventual recovery by the coherent target projections makes the completed limit map injective.

theorem ScottishBook155.DirectedLimitStage.eventualRecovery_of_bounded {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (targetProjection : CoherentRetractionLimit.ProjectionSystem N eN) {L : ℝ} (hL : 0 < L) (boundedRecovery : ∀ (a : ι) (x : Source M eM), dist x (CoherentRetractionLimit.ProjectionSystem.approx M eM sourceProjection a x) ≤ L → (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)) (x : Source M eM) : ∀ᶠ (a : ι) in Filter.atTop, (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)

A positive uniform recovery band implies the eventual recovery hypothesis needed for injectivity.

theorem ScottishBook155.DirectedLimitStage.eventualRecovery_of_bounded_lt {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (targetProjection : CoherentRetractionLimit.ProjectionSystem N eN) {L : ℝ} (hL : 0 < L) (boundedRecovery : ∀ (a : ι) (x : Source M eM), dist x (CoherentRetractionLimit.ProjectionSystem.approx M eM sourceProjection a x) < L → (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)) (x : Source M eM) : ∀ᶠ (a : ι) in Filter.atTop, (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)

Open-band version of eventualRecovery_of_bounded.

noncomputable def ScottishBook155.DirectedLimitStage.toProtectedStage {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (targetProjection : CoherentRetractionLimit.ProjectionSystem N eN) {r : ℝ} (stageInjective : ∀ (i : ι), Function.Injective (V i)) (stagePreserves : ∀ (i : ι), PreservesUpTo r (V i)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) (eventualRecovery : ∀ (x : Source M eM), ∀ᶠ (a : ι) in Filter.atTop, (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)) : ProtectedStage r

The completed directed limit is another protected stage.

Equations

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

noncomputable def ScottishBook155.DirectedLimitStage.toProtectedStageOfBounded {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (targetProjection : CoherentRetractionLimit.ProjectionSystem N eN) {r L : ℝ} (hL : 0 < L) (stageInjective : ∀ (i : ι), Function.Injective (V i)) (stagePreserves : ∀ (i : ι), PreservesUpTo r (V i)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) (boundedRecovery : ∀ (a : ι) (x : Source M eM), dist x (CoherentRetractionLimit.ProjectionSystem.approx M eM sourceProjection a x) ≤ L → (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)) : ProtectedStage r

Version of toProtectedStage using the uniform bounded-recovery invariant maintained by the recursion.

Equations

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

noncomputable def ScottishBook155.DirectedLimitStage.toProtectedStageOfBoundedLt {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [∀ (i : ι), CompleteSpace (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] [∀ (i : ι), CompleteSpace (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (sourceProjection : CoherentRetractionLimit.ProjectionSystem M eM) (targetProjection : CoherentRetractionLimit.ProjectionSystem N eN) {r L : ℝ} (hL : 0 < L) (stageInjective : ∀ (i : ι), Function.Injective (V i)) (stagePreserves : ∀ (i : ι), PreservesUpTo r (V i)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) (boundedRecovery : ∀ (a : ι) (x : Source M eM), dist x (CoherentRetractionLimit.ProjectionSystem.approx M eM sourceProjection a x) < L → (CoherentRetractionLimit.ProjectionFamily.completedProjection N eN (CoherentRetractionLimit.ProjectionSystem.family N eN targetProjection a)) (limitMap M N eM eN V x) = V a ((CoherentRetractionLimit.ProjectionFamily.completedProjection M eM (CoherentRetractionLimit.ProjectionSystem.family M eM sourceProjection a)) x)) : ProtectedStage r

Version of toProtectedStage for an open uniform recovery band.

Equations

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