AmplifiedRepair.lean

1 import KomorebiSpace.AmplifiedHolonomy
2 import KomorebiSpace.KernelProjectionBounds
3 import KomorebiSpace.Correction
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Exact reconstruction with nonisometric amplification
9 
10 Both forward normalization and inverse route restoration enter the gain.
11 The fiber's finite-dimensional inner product supplies the anchor projection;
12 the vertex and edge products retain their maximum norms.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace AmplifiedTransport
18 namespace Rooted
19 variable {V : Type u} {H : Type v}
20 variable [NormedAddCommGroup H] [NormedSpace ℝ H] [Fintype V]
21 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
22 variable (p : OverlapTransport.Routing graph o)
23 
24 /-- Bring each edge's residual back to the root coordinate frame. -/
25 def normalizer : (OverlapTransport.Edges graph → H) →L[ℝ]
26     (OverlapTransport.Edges graph → H) :=
27   ContinuousLinearMap.pi fun a =>
28     ((frame T p a.val.1).symm.toContinuousLinearMap).comp (ContinuousLinearMap.proj a : (OverlapTransport.Edges graph → H) →L[ℝ] H)
29 
30 omit [Fintype V] in
31 @[simp] theorem normalizer_apply (r : OverlapTransport.Edges graph → H)
32     (a : OverlapTransport.Edges graph) :
33     normalizer T p r a = (frame T p a.val.1).symm (r a) := rfl
34 
35 def rootResidualMap : H →L[ℝ] (OverlapTransport.Edges graph → H) :=
36   ContinuousLinearMap.pi fun a =>
37     (holonomy T p a).toContinuousLinearMap - ContinuousLinearMap.id ℝ H
38 
39 omit [Fintype V] in
40 @[simp] theorem rootResidualMap_apply (z : H) (a : OverlapTransport.Edges graph) :
41     rootResidualMap T p z a = holonomy T p a z-z := rfl
42 
43 omit [Fintype V] in
44 theorem rootResidualMap_kernel : (rootResidualMap T p).ker = fixedSpace T p := by
45   ext z
46   change rootResidualMap T p z = 0 ↔ _
47   constructor
48   · intro h a
49     exact sub_eq_zero.mp (congrFun h a)
50   · intro h
51     funext a
52     exact sub_eq_zero.mpr (h a)
53 
54 /-- The root operator is tied to the actual graph differential. -/
55 theorem normalized_reconstruction (z : H) :
56     normalizer T p (T.differential graph (reconstruct T p z)) = rootResidualMap T p z := by
57   funext a
58   exact normalized_reconstruction_defect T p z a
59 
60 theorem rootResidual_anchor_bound (x : V → H) :
61     ‖rootResidualMap T p (x o)‖ ≤
62       ‖normalizer T p‖ * (‖T.differential graph‖ * routeGain T p + 1) *
63         ‖T.differential graph x‖ := by
64   have herror : ‖reconstruct T p (x o)-x‖ ≤
65       routeGain T p * ‖T.differential graph x‖ := by
66     rw [norm_sub_rev]
67     exact anchored_approximation_bound T p x
68   have hd : ‖T.differential graph (reconstruct T p (x o))‖ ≤
69       (‖T.differential graph‖ * routeGain T p + 1) * ‖T.differential graph x‖ := by
70     calc
71       _ ≤ ‖T.differential graph (reconstruct T p (x o))-T.differential graph x‖ +
72           ‖T.differential graph x‖ := norm_le_norm_sub_add _ _
73       _ = ‖T.differential graph (reconstruct T p (x o)-x)‖ +
74           ‖T.differential graph x‖ := by rw [map_sub]
75       _ ≤ ‖T.differential graph‖ * ‖reconstruct T p (x o)-x‖ +
76           ‖T.differential graph x‖ := add_le_add ((T.differential graph).le_opNorm _) le_rfl
77       _ ≤ ‖T.differential graph‖ * (routeGain T p * ‖T.differential graph x‖) +
78           ‖T.differential graph x‖ :=
79         add_le_add (mul_le_mul_of_nonneg_left herror (norm_nonneg _)) le_rfl
80       _ = _ := by ring
81   rw [← normalized_reconstruction]
82   exact ((normalizer T p).le_opNorm _).trans
83     ((mul_le_mul_of_nonneg_left hd (norm_nonneg _)).trans_eq (by ring))
84 
85 /-- The original prescribed-observation correction problem, now with amplified bonds. -/
86 def problem (U : Set V) : CorrectionProblem (V → H)
87     (OverlapTransport.Edges graph → H) (U → H) where
88   residual := (T.differential graph).toLinearMap.toAddMonoidHom
89   semantics :=
90     { toFun := fun x i => x i.val
91       map_zero' := rfl
92       map_add' := by intros; rfl }
93 
94 theorem obstruction_criterion (U : Set V) (ho : o ∈ U) (x : V → H) :
95     (problem T (graph := graph) U).obstruction x = 0 ↔
96       x o ∈ fixedSpace T p ∧ ∀ i : U, reconstruct T p (x o) i.val = x i.val := by
97   rw [(problem T (graph := graph) U).flatten_iff]
98   constructor
99   · rintro ⟨y, hy, hp⟩
100     have hpar : T.Parallel graph y := (T.parallel_iff_differential_zero y).mpr hy
101     have ha : y o = x o := congrFun hp ⟨o,ho⟩
102     constructor
103     · rw [← ha]; exact parallel_anchor_fixed T p y hpar
104     · intro i
105       rw [← ha, parallel_reconstruction T p y hpar]
106       exact congrFun hp i
107   · rintro ⟨hf,hp⟩
108     exact ⟨reconstruct T p (x o), (T.parallel_iff_differential_zero _).mp
109       ((reconstruct_parallel_iff T p _).mpr hf), funext hp⟩
110 
111 theorem quantitative_prescribed_repair (U : Set V) (ho : o ∈ U) (x : V → H)
112     (hx : (problem T (graph := graph) U).obstruction x = 0) :
113     ∃! y : V → H, T.Parallel graph y ∧ (∀ i : U, y i.val = x i.val) ∧
114       ‖x-y‖ ≤ routeGain T p * ‖T.differential graph x‖ := by
115   obtain ⟨hf,hp⟩ := (obstruction_criterion T p U ho x).mp hx
116   refine ⟨reconstruct T p (x o), ⟨(reconstruct_parallel_iff T p _).mpr hf,
117     hp, anchored_approximation_bound T p x⟩, ?_⟩
118   intro y hy
119   exact parallel_unique T p hy.1 ((reconstruct_parallel_iff T p _).mpr hf)
120     ((hy.2.1 ⟨o,ho⟩).trans (reconstruct_anchor T p _).symm)
121 
122 end Rooted
123 end AmplifiedTransport
124 end KomorebiSpace
125 end
126 
127 noncomputable section
128 namespace KomorebiSpace
129 namespace AmplifiedTransport
130 namespace Rooted
131 variable {V : Type u} {H : Type v}
132 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H] [Fintype V]
133 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
134 variable (p : OverlapTransport.Routing graph o)
135 
136 /-- Orthogonality is on the anchor fiber, not the vertex maximum norm. -/
137 def anchorProjection : H →L[ℝ] H := KernelProjection.projection (rootResidualMap T p)
138 
139 def holonomyGain : ℝ := KernelProjection.gain (rootResidualMap T p)
140 
141 theorem holonomyGain_nonneg : 0 ≤ holonomyGain T p :=
142   KernelProjection.gain_nonneg (rootResidualMap T p)
143 
144 theorem anchorProjection_fixed (z : H) : anchorProjection T p z ∈ fixedSpace T p := by
145   rw [← rootResidualMap_kernel]
146   exact KernelProjection.projection_mem (rootResidualMap T p) z
147 
148 @[simp] theorem anchorProjection_fixes (z : H) (hz : z ∈ fixedSpace T p) :
149     anchorProjection T p z = z := by
150   apply KernelProjection.projection_fixes
151   change z ∈ (rootResidualMap T p).ker
152   rw [rootResidualMap_kernel]
153   exact hz
154 
155 @[simp] theorem anchorProjection_idempotent (z : H) :
156     anchorProjection T p (anchorProjection T p z) = anchorProjection T p z :=
157   anchorProjection_fixes T p _ (anchorProjection_fixed T p z)
158 
159 theorem anchorProjection_norm (z : H) : ‖anchorProjection T p z‖ ≤ ‖z‖ :=
160   KernelProjection.projection_norm (rootResidualMap T p) z
161 
162 theorem anchorProjection_error (z : H) :
163     ‖z-anchorProjection T p z‖ ≤ holonomyGain T p * ‖rootResidualMap T p z‖ :=
164   KernelProjection.error_bound (rootResidualMap T p) z
165 
166 /-- Every factor is constructed from the connection, routes and specified norms. -/
167 def stabilityGain : ℝ := routeGain T p +
168   ‖reconstructMap T p‖ * holonomyGain T p * ‖normalizer T p‖ *
169     (‖T.differential graph‖ * routeGain T p + 1)
170 
171 theorem stabilityGain_nonneg : 0 ≤ stabilityGain T p := by
172   unfold stabilityGain
173   have ha := routeGain_nonneg T p
174   have hk := holonomyGain_nonneg T p
175   positivity
176 
177 def orthogonalRepair : (V → H) →L[ℝ] (V → H) :=
178   (reconstructMap T p).comp ((anchorProjection T p).comp (ContinuousLinearMap.proj o))
179 
180 @[simp] theorem orthogonalRepair_apply (x : V → H) :
181     orthogonalRepair T p x = reconstruct T p (anchorProjection T p (x o)) := rfl
182 
183 @[simp] theorem orthogonalRepair_anchor (x : V → H) :
184     orthogonalRepair T p x o = anchorProjection T p (x o) := reconstruct_anchor T p _
185 
186 theorem orthogonalRepair_parallel (x : V → H) : T.Parallel graph (orthogonalRepair T p x) :=
187   (reconstruct_parallel_iff T p _).mpr (anchorProjection_fixed T p (x o))
188 
189 @[simp] theorem orthogonalRepair_fixes (x : V → H) (hx : T.Parallel graph x) :
190     orthogonalRepair T p x = x := by
191   rw [orthogonalRepair_apply, anchorProjection_fixes T p _ (parallel_anchor_fixed T p x hx)]
192   exact parallel_reconstruction T p x hx
193 
194 @[simp] theorem orthogonalRepair_idempotent (x : V → H) :
195     orthogonalRepair T p (orthogonalRepair T p x) = orthogonalRepair T p x :=
196   orthogonalRepair_fixes T p _ (orthogonalRepair_parallel T p x)
197 
198 /-- Unlike the isometric case, this projector is not asserted nonexpansive. -/
199 theorem orthogonalRepair_norm (x : V → H) :
200     ‖orthogonalRepair T p x‖ ≤ ‖reconstructMap T p‖ * ‖x‖ :=
201   (reconstruct_bound T p _).trans (mul_le_mul_of_nonneg_left
202     ((anchorProjection_norm T p _).trans (norm_le_pi_norm x o)) (norm_nonneg (reconstructMap T p)))
203 
204 theorem orthogonalRepair_error (x : V → H) :
205     ‖x-orthogonalRepair T p x‖ ≤ stabilityGain T p * ‖T.differential graph x‖ := by
206   have ha := anchorProjection_error T p (x o)
207   have hh := rootResidual_anchor_bound T p x
208   have hm := mul_le_mul_of_nonneg_left hh (holonomyGain_nonneg T p)
209   have hq := ha.trans hm
210   calc
211     _ ≤ routeGain T p * ‖T.differential graph x‖ +
212         ‖reconstructMap T p‖ * ‖x o-anchorProjection T p (x o)‖ :=
213       changed_anchor_error T p x _
214     _ ≤ routeGain T p * ‖T.differential graph x‖ +
215         ‖reconstructMap T p‖ * (holonomyGain T p *
216         (‖normalizer T p‖ * (‖T.differential graph‖ * routeGain T p + 1) *
217          ‖T.differential graph x‖)) :=
218       add_le_add le_rfl (mul_le_mul_of_nonneg_left hq (norm_nonneg (reconstructMap T p)))
219     _ = _ := by unfold stabilityGain; ring
220 
221 theorem orthogonalRepair_unique (x : V → H) :
222     ∃! y : V → H, T.Parallel graph y ∧
223       anchorProjection T p (y o) = anchorProjection T p (x o) := by
224   refine ⟨orthogonalRepair T p x, ⟨orthogonalRepair_parallel T p x, ?_⟩, ?_⟩
225   · rw [orthogonalRepair_anchor, anchorProjection_idempotent]
226   · intro y hy
227     apply parallel_unique T p hy.1 (orthogonalRepair_parallel T p x)
228     rw [orthogonalRepair_anchor]
229     rw [anchorProjection_fixes T p _ (parallel_anchor_fixed T p y hy.1)] at hy
230     exact hy.2
231 
232 theorem anchorProjection_route_independent (q : OverlapTransport.Routing graph o) :
233     anchorProjection T p = anchorProjection T q := by
234   apply KernelProjection.projection_eq_of_kernel_eq
235   rw [rootResidualMap_kernel, rootResidualMap_kernel, fixedSpace_route_independent T p q]
236 
237 theorem orthogonalRepair_route_independent (q : OverlapTransport.Routing graph o) :
238     orthogonalRepair T p = orthogonalRepair T q := by
239   ext x i
240   change reconstruct T p (anchorProjection T p (x o)) i =
241     reconstruct T q (anchorProjection T q (x o)) i
242   rw [← anchorProjection_route_independent T p q]
243   exact congrFun (reconstruction_route_independent T p q _
244     (anchorProjection_fixed T p (x o))) i
245 
246 end Rooted
247 end AmplifiedTransport
248 end KomorebiSpace
249 end

Back to source controls