HolonomyProjection.lean

1 import KomorebiSpace.HolonomyViews
2 import KomorebiSpace.KernelProjectionBounds
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Derived orthogonal anchor repair for finite-dimensional holonomy
8 
9 This instantiates the finite-dimensional kernel bound on the actual rooted
10 loop differential. The anchor correction and its finite gain are constructed,
11 not supplied as hypotheses. Vertex and edge products keep their old maximum
12 norms; only the individual fiber now has an inner-product norm.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace HolonomyTransport
18 namespace Rooted
19 variable {V : Type u} {H : Type v}
20 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H]
21 variable [Fintype V]
22 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
23 variable (p : OverlapTransport.Routing graph o)
24 
25 /-- The same loop residual as v0.18, bundled as a continuous linear map. -/
26 def rootResidualMap : H →L[ℝ] (OverlapTransport.Edges graph → H) :=
27   ContinuousLinearMap.pi fun a =>
28     (holonomy T p a).toContinuousLinearMap - ContinuousLinearMap.id ℝ H
29 
30 omit [Fintype V] in
31 @[simp] theorem rootResidualMap_apply (z : H) :
32     rootResidualMap T p z = rootResidual T p z := rfl
33 
34 omit [Fintype V] in
35 theorem rootResidualMap_kernel : (rootResidualMap T p).ker = fixedSpace T p := by
36   ext z
37   exact rootResidual_zero_iff T p z
38 
39 /-- Orthogonal projection onto the actual loop-compatible anchor vectors. -/
40 def anchorProjection : H →L[ℝ] H := KernelProjection.projection (rootResidualMap T p)
41 
42 /-- The inverse norm on complementary directions, with the original edge max norm. -/
43 def holonomyGain : ℝ := KernelProjection.gain (rootResidualMap T p)
44 
45 theorem holonomyGain_nonneg : 0 ≤ holonomyGain T p :=
46   KernelProjection.gain_nonneg (rootResidualMap T p)
47 
48 theorem anchorProjection_fixed (z : H) : anchorProjection T p z ∈ fixedSpace T p := by
49   rw [← rootResidualMap_kernel]
50   exact KernelProjection.projection_mem (rootResidualMap T p) z
51 
52 @[simp] theorem anchorProjection_fixes (z : H) (hz : z ∈ fixedSpace T p) :
53     anchorProjection T p z = z :=
54   KernelProjection.projection_fixes (rootResidualMap T p) z
55     ((rootResidual_zero_iff T p z).mpr hz)
56 
57 @[simp] theorem anchorProjection_idempotent (z : H) :
58     anchorProjection T p (anchorProjection T p z) = anchorProjection T p z :=
59   anchorProjection_fixes T p _ (anchorProjection_fixed T p z)
60 
61 theorem anchorProjection_norm (z : H) : ‖anchorProjection T p z‖ ≤ ‖z‖ :=
62   KernelProjection.projection_norm (rootResidualMap T p) z
63 
64 /-- The separate anchor-estimate obligation from v0.18 is discharged here. -/
65 theorem anchorProjection_error (z : H) :
66     ‖z-anchorProjection T p z‖ ≤ holonomyGain T p * ‖rootResidual T p z‖ :=
67   KernelProjection.error_bound (rootResidualMap T p) z
68 
69 theorem anchorProjection_best (z w : H) (hw : w ∈ fixedSpace T p) :
70     ‖z-anchorProjection T p z‖ ≤ ‖z-w‖ :=
71   KernelProjection.projection_best (rootResidualMap T p) z w
72     ((rootResidual_zero_iff T p w).mpr hw)
73 
74 theorem holonomyGain_optimal (C : ℝ) (hC : 0 ≤ C) :
75     (∀ z, ‖z-anchorProjection T p z‖ ≤ C * ‖rootResidual T p z‖) ↔
76       holonomyGain T p ≤ C :=
77   KernelProjection.gain_characterization (rootResidualMap T p) C hC
78 
79 /-- The projection is independent of root routes, for a fixed root and inner product. -/
80 theorem anchorProjection_route_independent (q : OverlapTransport.Routing graph o) :
81     anchorProjection T p = anchorProjection T q := by
82   apply KernelProjection.projection_eq_of_kernel_eq
83   rw [rootResidualMap_kernel, rootResidualMap_kernel,
84     fixedSpace_route_independent T p q]
85 
86 /-- Route reconstruction as a bounded linear map into the existing vertex max norm. -/
87 def reconstructMap : H →L[ℝ] (V → H) :=
88   ContinuousLinearMap.pi fun i => (frame T p i).toContinuousLinearMap
89 
90 omit [Fintype V] in
91 @[simp] theorem reconstructMap_apply (z : H) : reconstructMap T p z = reconstruct T p z := rfl
92 
93 /-- Canonical anchor correction followed by the actual graph reconstruction. -/
94 def orthogonalRepair : (V → H) →L[ℝ] (V → H) :=
95   (reconstructMap T p).comp ((anchorProjection T p).comp (ContinuousLinearMap.proj o))
96 
97 @[simp] theorem orthogonalRepair_apply (x : V → H) :
98     orthogonalRepair T p x = reconstruct T p (anchorProjection T p (x o)) := rfl
99 
100 @[simp] theorem orthogonalRepair_anchor (x : V → H) :
101     orthogonalRepair T p x o = anchorProjection T p (x o) :=
102   reconstruct_anchor T p _
103 
104 theorem orthogonalRepair_parallel (x : V → H) : T.Parallel graph (orthogonalRepair T p x) :=
105   (reconstruct_parallel_iff T p _).mpr (anchorProjection_fixed T p (x o))
106 
107 @[simp] theorem orthogonalRepair_fixes (x : V → H) (hx : T.Parallel graph x) :
108     orthogonalRepair T p x = x := by
109   rw [orthogonalRepair_apply, anchorProjection_fixes T p _ (parallel_anchor_fixed T p x hx)]
110   exact parallel_reconstruction T p x hx
111 
112 @[simp] theorem orthogonalRepair_idempotent (x : V → H) :
113     orthogonalRepair T p (orthogonalRepair T p x) = orthogonalRepair T p x :=
114   orthogonalRepair_fixes T p _ (orthogonalRepair_parallel T p x)
115 
116 theorem orthogonalRepair_norm (x : V → H) : ‖orthogonalRepair T p x‖ ≤ ‖x‖ := by
117   rw [orthogonalRepair_apply, reconstruct_norm]
118   exact (anchorProjection_norm T p (x o)).trans (norm_le_pi_norm x o)
119 
120 theorem orthogonalRepair_opNorm : ‖orthogonalRepair T p‖ ≤ 1 := by
121   apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one
122   intro x
123   simpa only [one_mul] using orthogonalRepair_norm T p x
124 
125 /-- Valid for every candidate, including those with inadmissible original anchors. -/
126 theorem orthogonalRepair_error (x : V → H) :
127     ‖x-orthogonalRepair T p x‖ ≤
128       ((p.radius : ℝ) + holonomyGain T p * (2*(p.radius : ℝ)+1)) *
129         ‖T.differential graph x‖ :=
130   (repair_from_anchor_estimate T p (anchorProjection T p) (holonomyGain T p)
131     (holonomyGain_nonneg T p) (anchorProjection_fixed T p) (anchorProjection_error T p) x).2
132 
133 /-- An exact candidate is uniquely determined by the feasible component of its anchor. -/
134 theorem orthogonalRepair_unique (x : V → H) :
135     ∃! y : V → H, T.Parallel graph y ∧
136       anchorProjection T p (y o) = anchorProjection T p (x o) := by
137   refine ⟨orthogonalRepair T p x, ⟨orthogonalRepair_parallel T p x, ?_⟩, ?_⟩
138   · rw [orthogonalRepair_anchor, anchorProjection_idempotent]
139   · intro y hy
140     apply parallel_unique T p hy.1 (orthogonalRepair_parallel T p x)
141     rw [orthogonalRepair_anchor]
142     rw [anchorProjection_fixes T p _ (parallel_anchor_fixed T p y hy.1)] at hy
143     exact hy.2
144 
145 theorem orthogonalRepair_route_independent (q : OverlapTransport.Routing graph o) :
146     orthogonalRepair T p = orthogonalRepair T q := by
147   ext x i
148   change reconstruct T p (anchorProjection T p (x o)) i =
149     reconstruct T q (anchorProjection T q (x o)) i
150   rw [← anchorProjection_route_independent T p q]
151   exact congrFun (reconstruction_route_independent T p q _
152     (anchorProjection_fixed T p (x o))) i
153 
154 /-- An actual old Ambient object, not a renamed numerical candidate. -/
155 def orthogonalAmbient (x : V → H) : (T.pathViews graph).Ambient :=
156   T.toAmbient graph (orthogonalRepair T p x) (orthogonalRepair_parallel T p x)
157 
158 theorem finite_dimensional_ambient_repair (x : V → H) :
159     ∃ s : (T.pathViews graph).Ambient,
160       anchorProjection T p (s.val ⟨o⟩) = anchorProjection T p (x o) ∧
161       ‖x-T.ambientValues graph s‖ ≤
162         ((p.radius : ℝ) + holonomyGain T p * (2*(p.radius : ℝ)+1)) *
163           ‖T.differential graph x‖ := by
164   refine ⟨orthogonalAmbient T p x, ?_, orthogonalRepair_error T p x⟩
165   change anchorProjection T p (orthogonalRepair T p x o) = _
166   rw [orthogonalRepair_anchor, anchorProjection_idempotent]
167 
168 /-- The quantified bound is derived for each fixed finite-dimensional system;
169 it is not a common constant over all connections. -/
170 theorem finite_dimensional_stability :
171     ∃ C : ℝ, 0 ≤ C ∧ ∀ x : V → H,
172       T.Parallel graph (orthogonalRepair T p x) ∧
173       ‖x-orthogonalRepair T p x‖ ≤ C * ‖T.differential graph x‖ := by
174   refine ⟨(p.radius : ℝ) + holonomyGain T p * (2*(p.radius : ℝ)+1), ?_,
175     fun x => ⟨orthogonalRepair_parallel T p x, orthogonalRepair_error T p x⟩⟩
176   have hg := holonomyGain_nonneg T p
177   positivity
178 
179 end Rooted
180 end HolonomyTransport
181 end KomorebiSpace
182 end

Back to source controls