HilbertHolonomyRepair.lean

1 import KomorebiSpace.AmplifiedViews
2 import KomorebiSpace.HilbertKernelProjection
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Infinite-dimensional amplified holonomy reconstruction
8 
9 The fiber is a real Hilbert space, not necessarily finite dimensional.
10 Orthogonal anchor repair exists without a range hypothesis. A global
11 residual-to-repair estimate holds precisely when the actual holonomy
12 operator has closed range. The old finite-dimensional repair is retained.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace AmplifiedTransport
18 namespace Rooted
19 namespace Hilbert
20 variable {V : Type u} {H : Type v}
21 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [Fintype V]
22 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
23 variable (p : OverlapTransport.Routing graph o)
24 
25 /-- Orthogonality is on the anchor fiber, not the vertex maximum norm. -/
26 def anchorProjection : H →L[ℝ] H := HilbertKernelProjection.projection (rootResidualMap T p)
27 
28 variable (hr : IsClosed (Set.range (rootResidualMap T p)))
29 
30 def holonomyGain : ℝ := HilbertKernelProjection.gain (rootResidualMap T p) hr
31 
32 theorem holonomyGain_nonneg : 0 ≤ holonomyGain T p hr :=
33   HilbertKernelProjection.gain_nonneg (rootResidualMap T p) hr
34 
35 theorem anchorProjection_fixed (z : H) : anchorProjection T p z ∈ fixedSpace T p := by
36   rw [← rootResidualMap_kernel]
37   exact HilbertKernelProjection.projection_mem (rootResidualMap T p) z
38 
39 @[simp] theorem anchorProjection_fixes (z : H) (hz : z ∈ fixedSpace T p) :
40     anchorProjection T p z = z := by
41   apply HilbertKernelProjection.projection_fixes
42   change z ∈ (rootResidualMap T p).ker
43   rw [rootResidualMap_kernel]
44   exact hz
45 
46 @[simp] theorem anchorProjection_idempotent (z : H) :
47     anchorProjection T p (anchorProjection T p z) = anchorProjection T p z :=
48   anchorProjection_fixes T p _ (anchorProjection_fixed T p z)
49 
50 theorem anchorProjection_norm (z : H) : ‖anchorProjection T p z‖ ≤ ‖z‖ :=
51   HilbertKernelProjection.projection_norm (rootResidualMap T p) z
52 
53 theorem anchorProjection_error (z : H) :
54     ‖z-anchorProjection T p z‖ ≤ holonomyGain T p hr * ‖rootResidualMap T p z‖ :=
55   HilbertKernelProjection.error_bound (rootResidualMap T p) hr z
56 
57 /-- Every factor is constructed from the connection, routes and specified norms. -/
58 def stabilityGain : ℝ := routeGain T p +
59   ‖reconstructMap T p‖ * holonomyGain T p hr * ‖normalizer T p‖ *
60     (‖T.differential graph‖ * routeGain T p + 1)
61 
62 theorem stabilityGain_nonneg : 0 ≤ stabilityGain T p hr := by
63   unfold stabilityGain
64   have ha := routeGain_nonneg T p
65   have hk := holonomyGain_nonneg T p hr
66   positivity
67 
68 def orthogonalRepair : (V → H) →L[ℝ] (V → H) :=
69   (reconstructMap T p).comp ((anchorProjection T p).comp (ContinuousLinearMap.proj o))
70 
71 @[simp] theorem orthogonalRepair_apply (x : V → H) :
72     orthogonalRepair T p x = reconstruct T p (anchorProjection T p (x o)) := rfl
73 
74 @[simp] theorem orthogonalRepair_anchor (x : V → H) :
75     orthogonalRepair T p x o = anchorProjection T p (x o) := reconstruct_anchor T p _
76 
77 theorem orthogonalRepair_parallel (x : V → H) : T.Parallel graph (orthogonalRepair T p x) :=
78   (reconstruct_parallel_iff T p _).mpr (anchorProjection_fixed T p (x o))
79 
80 @[simp] theorem orthogonalRepair_fixes (x : V → H) (hx : T.Parallel graph x) :
81     orthogonalRepair T p x = x := by
82   rw [orthogonalRepair_apply, anchorProjection_fixes T p _ (parallel_anchor_fixed T p x hx)]
83   exact parallel_reconstruction T p x hx
84 
85 @[simp] theorem orthogonalRepair_idempotent (x : V → H) :
86     orthogonalRepair T p (orthogonalRepair T p x) = orthogonalRepair T p x :=
87   orthogonalRepair_fixes T p _ (orthogonalRepair_parallel T p x)
88 
89 /-- Unlike the isometric case, this projector is not asserted nonexpansive. -/
90 theorem orthogonalRepair_norm (x : V → H) :
91     ‖orthogonalRepair T p x‖ ≤ ‖reconstructMap T p‖ * ‖x‖ :=
92   (reconstruct_bound T p _).trans (mul_le_mul_of_nonneg_left
93     ((anchorProjection_norm T p _).trans (norm_le_pi_norm x o)) (norm_nonneg (reconstructMap T p)))
94 
95 theorem orthogonalRepair_error (x : V → H) :
96     ‖x-orthogonalRepair T p x‖ ≤ stabilityGain T p hr * ‖T.differential graph x‖ := by
97   have ha := anchorProjection_error T p hr (x o)
98   have hh := rootResidual_anchor_bound T p x
99   have hm := mul_le_mul_of_nonneg_left hh (holonomyGain_nonneg T p hr)
100   have hq := ha.trans hm
101   calc
102     _ ≤ routeGain T p * ‖T.differential graph x‖ +
103         ‖reconstructMap T p‖ * ‖x o-anchorProjection T p (x o)‖ :=
104       changed_anchor_error T p x _
105     _ ≤ routeGain T p * ‖T.differential graph x‖ +
106         ‖reconstructMap T p‖ * (holonomyGain T p hr *
107         (‖normalizer T p‖ * (‖T.differential graph‖ * routeGain T p + 1) *
108          ‖T.differential graph x‖)) :=
109       add_le_add le_rfl (mul_le_mul_of_nonneg_left hq (norm_nonneg (reconstructMap T p)))
110     _ = _ := by unfold stabilityGain; ring
111 
112 theorem orthogonalRepair_unique (x : V → H) :
113     ∃! y : V → H, T.Parallel graph y ∧
114       anchorProjection T p (y o) = anchorProjection T p (x o) := by
115   refine ⟨orthogonalRepair T p x, ⟨orthogonalRepair_parallel T p x, ?_⟩, ?_⟩
116   · rw [orthogonalRepair_anchor, anchorProjection_idempotent]
117   · intro y hy
118     apply parallel_unique T p hy.1 (orthogonalRepair_parallel T p x)
119     rw [orthogonalRepair_anchor]
120     rw [anchorProjection_fixes T p _ (parallel_anchor_fixed T p y hy.1)] at hy
121     exact hy.2
122 
123 theorem anchorProjection_route_independent (q : OverlapTransport.Routing graph o) :
124     anchorProjection T p = anchorProjection T q := by
125   apply HilbertKernelProjection.projection_eq_of_kernel_eq
126   rw [rootResidualMap_kernel, rootResidualMap_kernel, fixedSpace_route_independent T p q]
127 
128 theorem orthogonalRepair_route_independent (q : OverlapTransport.Routing graph o) :
129     orthogonalRepair T p = orthogonalRepair T q := by
130   ext x i
131   change reconstruct T p (anchorProjection T p (x o)) i =
132     reconstruct T q (anchorProjection T q (x o)) i
133   rw [← anchorProjection_route_independent T p q]
134   exact congrFun (reconstruction_route_independent T p q _
135     (anchorProjection_fixed T p (x o))) i
136 
137 
138 /-- Inverse normalization on the actual directed-edge residual space. -/
139 def denormalizer : (OverlapTransport.Edges graph → H) →L[ℝ]
140     (OverlapTransport.Edges graph → H) :=
141   ContinuousLinearMap.pi fun a =>
142     (frame T p a.val.1).toContinuousLinearMap.comp
143       (ContinuousLinearMap.proj a : (OverlapTransport.Edges graph → H) →L[ℝ] H)
144 
145 omit [CompleteSpace H] [Fintype V] in
146 @[simp] theorem denormalizer_normalizer (r : OverlapTransport.Edges graph → H) :
147     denormalizer T p (normalizer T p r) = r := by
148   funext a
149   exact (frame T p a.val.1).apply_symm_apply (r a)
150 
151 omit [CompleteSpace H] in
152 /-- Reconstructed edge defects and root defects differ only by bounded normalization. -/
153 theorem differential_reconstruct (z : H) :
154     T.differential graph (reconstruct T p z) =
155       denormalizer T p (rootResidualMap T p z) := by
156   rw [← normalized_reconstruction T p z, denormalizer_normalizer]
157 
158 /-- A global estimate would in particular control the root's orthogonal displacement. -/
159 theorem closed_range_of_global_bound (C : ℝ) (hC : 0 ≤ C)
160     (hb : ∀ x : V → H, ‖x-orthogonalRepair T p x‖ ≤
161       C * ‖T.differential graph x‖) :
162     IsClosed (Set.range (rootResidualMap T p)) := by
163   apply HilbertKernelProjection.closed_range_of_bound (rootResidualMap T p)
164     (C * ‖denormalizer T p‖) (mul_nonneg hC (norm_nonneg (denormalizer T p)))
165   intro z
166   have he : ‖z-anchorProjection T p z‖ ≤
167       ‖reconstruct T p z-orthogonalRepair T p (reconstruct T p z)‖ := by
168     simpa only [Pi.sub_apply, reconstruct_anchor, orthogonalRepair_anchor]
169       using norm_le_pi_norm
170         (reconstruct T p z-orthogonalRepair T p (reconstruct T p z)) o
171   calc
172     _ ≤ ‖reconstruct T p z-orthogonalRepair T p (reconstruct T p z)‖ := he
173     _ ≤ C * ‖T.differential graph (reconstruct T p z)‖ := hb _
174     _ = C * ‖denormalizer T p (rootResidualMap T p z)‖ := by
175       rw [differential_reconstruct]
176     _ ≤ C * (‖denormalizer T p‖ * ‖rootResidualMap T p z‖) :=
177       mul_le_mul_of_nonneg_left ((denormalizer T p).le_opNorm _) hC
178     _ = _ := by ring
179 
180 /-- Closed holonomy range is necessary and sufficient for a finite global repair gain. -/
181 theorem closed_range_iff_global_bound :
182     IsClosed (Set.range (rootResidualMap T p)) ↔
183       ∃ C : ℝ, 0 ≤ C ∧ ∀ x : V → H,
184         ‖x-orthogonalRepair T p x‖ ≤ C * ‖T.differential graph x‖ := by
185   constructor
186   · intro h
187     exact ⟨stabilityGain T p h, stabilityGain_nonneg T p h,
188       orthogonalRepair_error T p h⟩
189   · rintro ⟨C,hC,hb⟩
190     exact closed_range_of_global_bound T p C hC hb
191 
192 /-- The criterion is not restricted to this chosen projector: any exact answer
193 with a uniform residual estimate would force the same closed range. -/
194 theorem closed_range_iff_near_parallel :
195     IsClosed (Set.range (rootResidualMap T p)) ↔
196       ∃ C : ℝ, 0 ≤ C ∧ ∀ x : V → H, ∃ y : V → H,
197         T.Parallel graph y ∧ ‖x-y‖ ≤ C * ‖T.differential graph x‖ := by
198   constructor
199   · intro h
200     exact ⟨stabilityGain T p h, stabilityGain_nonneg T p h, fun x =>
201       ⟨orthogonalRepair T p x, orthogonalRepair_parallel T p x,
202         orthogonalRepair_error T p h x⟩⟩
203   · rintro ⟨C,hC,hb⟩
204     apply HilbertKernelProjection.closed_range_of_bound (rootResidualMap T p)
205       (C * ‖denormalizer T p‖) (mul_nonneg hC (norm_nonneg (denormalizer T p)))
206     intro z
207     obtain ⟨y,hy,he⟩ := hb (reconstruct T p z)
208     have hzero : rootResidualMap T p (y o) = 0 := by
209       change y o ∈ (rootResidualMap T p).ker
210       rw [rootResidualMap_kernel]
211       exact parallel_anchor_fixed T p y hy
212     calc
213       _ ≤ ‖z-y o‖ := HilbertKernelProjection.projection_best (rootResidualMap T p) z (y o) hzero
214       _ ≤ ‖reconstruct T p z-y‖ := by
215         simpa only [Pi.sub_apply,reconstruct_anchor] using
216           norm_le_pi_norm (reconstruct T p z-y) o
217       _ ≤ C * ‖T.differential graph (reconstruct T p z)‖ := he
218       _ = C * ‖denormalizer T p (rootResidualMap T p z)‖ := by
219         rw [differential_reconstruct]
220       _ ≤ C * (‖denormalizer T p‖ * ‖rootResidualMap T p z‖) :=
221         mul_le_mul_of_nonneg_left ((denormalizer T p).le_opNorm _) hC
222       _ = _ := by ring
223 
224 /-- Closed-range stability, unlike a selected numerical upper bound, is route-independent. -/
225 theorem closed_range_route_independent (q : OverlapTransport.Routing graph o) :
226     IsClosed (Set.range (rootResidualMap T p)) ↔
227       IsClosed (Set.range (rootResidualMap T q)) := by
228   rw [closed_range_iff_global_bound T p, closed_range_iff_global_bound T q,
229     orthogonalRepair_route_independent T p q]
230 
231 /-- The reconstructed exact object lives in the previous ambient-section type. -/
232 def orthogonalAmbient (x : V → H) : (T.pathViews graph).Ambient :=
233   T.toAmbient graph (orthogonalRepair T p x) (orthogonalRepair_parallel T p x)
234 
235 theorem closed_range_ambient_repair (x : V → H) :
236     ∃ s : (T.pathViews graph).Ambient,
237       anchorProjection T p (s.val ⟨o⟩) = anchorProjection T p (x o) ∧
238       ‖x-T.ambientValues graph s‖ ≤ stabilityGain T p hr * ‖T.differential graph x‖ := by
239   refine ⟨orthogonalAmbient T p x, ?_, orthogonalRepair_error T p hr x⟩
240   change anchorProjection T p (orthogonalRepair T p x o) = _
241   rw [orthogonalRepair_anchor, anchorProjection_idempotent]
242 
243 /-- Finite-dimensional v0.20 repair is definitionally the same projector. -/
244 theorem finite_dimensional_agreement [FiniteDimensional ℝ H] :
245     orthogonalRepair T p = KomorebiSpace.AmplifiedTransport.Rooted.orthogonalRepair T p := rfl
246 
247 end Hilbert
248 end Rooted
249 end AmplifiedTransport
250 end KomorebiSpace
251 end

Back to source controls