GraphResidual.lean

1 import PaperXI.ContinuousHolonomyResidual
2 import PaperXI.GraphTransport
3 import PaperXI.GraphTree
4 import Mathlib.Analysis.Normed.Module.FiniteDimension
5 
6 /-! Paper XI, 14.6 and 14.7 on the actual rooted graph paths. Finite dimensionality
7 makes the given edge equivalences and their actual inverses continuous for the
8 specified norms. Parallel edges and self-loops keep their identities. -/
9 set_option autoImplicit false
10 noncomputable section
11 
12 namespace PaperXI.GraphResidual
13 
14 open Quiver GraphTree
15 
16 variable {α : Type*} [Quiver α]
17 variable {V W : α → Type*}
18 variable [∀ u, NormedAddCommGroup (V u)] [∀ u, NormedSpace ℂ (V u)]
19 variable [∀ u, FiniteDimensional ℂ (V u)]
20 variable [∀ u, NormedAddCommGroup (W u)] [∀ u, NormedSpace ℂ (W u)]
21 variable [∀ u, FiniteDimensional ℂ (W u)]
22 
23 /-- The bounded transport is exactly the algebraic transport on the given walk. -/
24 def pathL (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
25     {u v : α} (p : GraphTransport.Walk u v) : V u ≃L[ℂ] V v :=
26   (GraphTransport.path A p).toContinuousLinearEquiv
27 
28 @[simp] theorem pathL_toLinearEquiv
29     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
30     {u v : α} (p : GraphTransport.Walk u v) :
31     (pathL A p).toLinearEquiv = GraphTransport.path A p := rfl
32 
33 @[simp] theorem pathL_apply
34     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
35     {u v : α} (p : GraphTransport.Walk u v) (x : V u) :
36     pathL A p x = GraphTransport.path A p x := rfl
37 
38 @[simp] theorem pathL_symm_apply
39     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
40     {u v : α} (p : GraphTransport.Walk u v) (x : V v) :
41     (pathL A p).symm x = (GraphTransport.path A p).symm x := rfl
42 
43 @[simp] theorem pathL_reverse
44     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
45     {u v : α} (p : GraphTransport.Walk u v) :
46     pathL A p.reverse = (pathL A p).symm := by
47   ext x
48   exact LinearEquiv.congr_fun (GraphTransport.reverse A p) x
49 
50 @[simp] theorem pathL_comp
51     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
52     {u v w : α} (p : GraphTransport.Walk u v) (q : GraphTransport.Walk v w) :
53     pathL A (p.comp q) = (pathL A p).trans (pathL A q) := by
54   ext x
55   exact LinearEquiv.congr_fun (GraphTransport.comp A p q) x
56 
57 variable {r : α}
58 
59 /-- The continuous vertex gauge is constructed from the actual tree paths. -/
60 def gauge (T : GraphTree.Rooted α r)
61     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
62     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
63     (U : V r ≃ₗ[ℂ] W r) (v : α) : V v ≃L[ℂ] W v :=
64   ContinuousHolonomyResidual.transported U.toContinuousLinearEquiv
65     (pathL A (GraphTree.rootPath T v)) (pathL B (GraphTree.rootPath T v))
66 
67 @[simp] theorem gauge_toLinearEquiv (T : GraphTree.Rooted α r)
68     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
69     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
70     (U : V r ≃ₗ[ℂ] W r) (v : α) :
71     (gauge T A B U v).toLinearEquiv = HolonomyResidual.transported U
72       (GraphTransport.path A (GraphTree.rootPath T v)) (GraphTransport.path B (GraphTree.rootPath T v)) := rfl
73 
74 @[simp] theorem gauge_apply (T : GraphTree.Rooted α r)
75     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
76     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
77     (U : V r ≃ₗ[ℂ] W r) (v : α) (x : V v) :
78     gauge T A B U v x = GraphTransport.path B (GraphTree.rootPath T v)
79       (U ((GraphTransport.path A (GraphTree.rootPath T v)).symm x)) := rfl
80 
81 @[simp] theorem gauge_root (T : GraphTree.Rooted α r)
82     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
83     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
84     (U : V r ≃ₗ[ℂ] W r) : gauge T A B U r = U.toContinuousLinearEquiv := by
85   ext x
86   simp only [gauge_apply, GraphTree.rootPath_root]
87   rfl
88 
89 /-- The constructed gauge satisfies the selected tree-edge equation. -/
90 theorem gauge_parent (T : GraphTree.Rooted α r)
91     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
92     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
93     (U : V r ≃ₗ[ℂ] W r) (a : {a : α // a ≠ r}) (x : V (T.parent a)) :
94     gauge T A B U a.val (GraphTransport.edge A (T.parentEdge a) x) =
95       GraphTransport.edge B (T.parentEdge a) (gauge T A B U (T.parent a) x) := by
96   simp only [gauge_apply]
97   rw [← GraphTree.rootPath_parent T a]
98   change GraphTransport.edge B (T.parentEdge a)
99     (GraphTransport.path B (GraphTree.rootPath T (T.parent a))
100       (U ((GraphTransport.path A (GraphTree.rootPath T (T.parent a))).symm
101         ((GraphTransport.edge A (T.parentEdge a)).symm
102           (GraphTransport.edge A (T.parentEdge a) x))))) = _
103   rw [LinearEquiv.symm_apply_apply]
104 
105 /-- The literal residual of the constructed gauges and original edge maps. -/
106 def edgeResidual (T : GraphTree.Rooted α r)
107     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
108     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
109     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) : V u →L[ℂ] W v :=
110   (gauge T A B U v).toContinuousLinearMap.comp
111       (A e).toContinuousLinearEquiv.toContinuousLinearMap -
112     (B e).toContinuousLinearEquiv.toContinuousLinearMap.comp
113       (gauge T A B U u).toContinuousLinearMap
114 
115 /-- The defect uses the actual tree transports and the actual edge. -/
116 def cycleDefect (T : GraphTree.Rooted α r)
117     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
118     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
119     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) : V r →L[ℂ] W r :=
120   ContinuousHolonomyResidual.cycleDefect U.toContinuousLinearEquiv
121     (pathL A (GraphTree.rootPath T u)) (pathL A (GraphTree.rootPath T v))
122     (pathL B (GraphTree.rootPath T u)) (pathL B (GraphTree.rootPath T v))
123     (A e).toContinuousLinearEquiv (B e).toContinuousLinearEquiv
124 
125 theorem cycleDefect_toLinearMap (T : GraphTree.Rooted α r)
126     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
127     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
128     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
129     (cycleDefect T A B U e).toLinearMap = HolonomyResidual.cycleDefect U
130       (GraphTransport.path A (GraphTree.rootPath T u)) (GraphTransport.path A (GraphTree.rootPath T v))
131       (GraphTransport.path B (GraphTree.rootPath T u)) (GraphTransport.path B (GraphTree.rootPath T v))
132       (A e) (B e) := rfl
133 
134 theorem edgeResidual_toLinearMap (T : GraphTree.Rooted α r)
135     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
136     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
137     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
138     (edgeResidual T A B U e).toLinearMap = HolonomyResidual.edgeResidual U
139       (GraphTransport.path A (GraphTree.rootPath T u)) (GraphTransport.path A (GraphTree.rootPath T v))
140       (GraphTransport.path B (GraphTree.rootPath T u)) (GraphTransport.path B (GraphTree.rootPath T v))
141       (A e) (B e) := rfl
142 
143 /-- The defect compares the transports on the literal based fundamental loop. -/
144 theorem cycleDefect_loop (T : GraphTree.Rooted α r)
145     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
146     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
147     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
148     (cycleDefect T A B U e).toLinearMap =
149       U.toLinearMap.comp (GraphTransport.path A
150         (((GraphTree.rootPath T u).cons (Sum.inl e)).comp (GraphTree.rootPath T v).reverse)).toLinearMap -
151       (GraphTransport.path B
152         (((GraphTree.rootPath T u).cons (Sum.inl e)).comp (GraphTree.rootPath T v).reverse)).toLinearMap.comp
153           U.toLinearMap := by
154   rw (config := { transparency := .all })
155     [GraphTransport.comp A, GraphTransport.comp B,
156       GraphTransport.reverse A, GraphTransport.reverse B,
157       GraphTransport.cons A, GraphTransport.cons B]
158   ext x
159   simp [cycleDefect, ContinuousHolonomyResidual.cycleDefect]
160 
161 /-- Exact graph identity, in particular valid for every non-tree edge. -/
162 theorem residual_factorization (T : GraphTree.Rooted α r)
163     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
164     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
165     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
166     edgeResidual T A B U e = (pathL B (GraphTree.rootPath T v)).toContinuousLinearMap.comp
167       ((cycleDefect T A B U e).comp (pathL A (GraphTree.rootPath T u)).symm.toContinuousLinearMap) :=
168   ContinuousHolonomyResidual.residual_factorization U.toContinuousLinearEquiv
169     (pathL A (GraphTree.rootPath T u)) (pathL A (GraphTree.rootPath T v))
170     (pathL B (GraphTree.rootPath T u)) (pathL B (GraphTree.rootPath T v))
171     (A e).toContinuousLinearEquiv (B e).toContinuousLinearEquiv
172 
173 theorem residual_zero_iff (T : GraphTree.Rooted α r)
174     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
175     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
176     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
177     edgeResidual T A B U e = 0 ↔ cycleDefect T A B U e = 0 :=
178   ContinuousHolonomyResidual.residual_zero_iff U.toContinuousLinearEquiv
179     (pathL A (GraphTree.rootPath T u)) (pathL A (GraphTree.rootPath T v))
180     (pathL B (GraphTree.rootPath T u)) (pathL B (GraphTree.rootPath T v))
181     (A e).toContinuousLinearEquiv (B e).toContinuousLinearEquiv
182 
183 /-- The precise bound has only the two path conditioning factors. -/
184 theorem residual_norm_bound (T : GraphTree.Rooted α r)
185     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
186     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
187     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
188     ‖edgeResidual T A B U e‖ ≤
189       ‖(pathL B (GraphTree.rootPath T v)).toContinuousLinearMap‖ * ‖cycleDefect T A B U e‖ *
190         ‖(pathL A (GraphTree.rootPath T u)).symm.toContinuousLinearMap‖ :=
191   ContinuousHolonomyResidual.residual_norm_bound U.toContinuousLinearEquiv
192     (pathL A (GraphTree.rootPath T u)) (pathL A (GraphTree.rootPath T v))
193     (pathL B (GraphTree.rootPath T u)) (pathL B (GraphTree.rootPath T v))
194     (A e).toContinuousLinearEquiv (B e).toContinuousLinearEquiv
195 
196 theorem uniform_bound (T : GraphTree.Rooted α r)
197     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
198     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
199     (U : V r ≃ₗ[ℂ] W r) (C_B ε C_A : ℝ)
200     (hB : ∀ v, ‖(pathL B (GraphTree.rootPath T v)).toContinuousLinearMap‖ ≤ C_B)
201     (hD : ∀ {u v : α} (e : u ⟶ v), ‖cycleDefect T A B U e‖ ≤ ε)
202     (hA : ∀ u, ‖(pathL A (GraphTree.rootPath T u)).symm.toContinuousLinearMap‖ ≤ C_A)
203     {u v : α} (e : u ⟶ v) :
204     ‖edgeResidual T A B U e‖ ≤ C_B * ε * C_A :=
205   ContinuousHolonomyResidual.uniform_bound U.toContinuousLinearEquiv
206     (pathL A (GraphTree.rootPath T u)) (pathL A (GraphTree.rootPath T v))
207     (pathL B (GraphTree.rootPath T u)) (pathL B (GraphTree.rootPath T v))
208     (A e).toContinuousLinearEquiv (B e).toContinuousLinearEquiv
209     C_B ε C_A (hB v) (hD e) (hA u)
210 
211 /-- Uniform control is a bound on the mixed factor, with both actual norms. -/
212 theorem uniform_product_bound (T : GraphTree.Rooted α r)
213     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
214     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
215     (U : V r ≃ₗ[ℂ] W r) (C ε : ℝ)
216     (hC : ∀ {u v : α} (_e : u ⟶ v),
217       ‖(pathL B (GraphTree.rootPath T v)).toContinuousLinearMap‖ *
218         ‖(pathL A (GraphTree.rootPath T u)).symm.toContinuousLinearMap‖ ≤ C)
219     (hD : ∀ {u v : α} (e : u ⟶ v), ‖cycleDefect T A B U e‖ ≤ ε)
220     {u v : α} (e : u ⟶ v) : ‖edgeResidual T A B U e‖ ≤ C * ε :=
221   ContinuousHolonomyResidual.product_conditioning_bound U.toContinuousLinearEquiv
222     (pathL A (GraphTree.rootPath T u)) (pathL A (GraphTree.rootPath T v))
223     (pathL B (GraphTree.rootPath T u)) (pathL B (GraphTree.rootPath T v))
224     (A e).toContinuousLinearEquiv (B e).toContinuousLinearEquiv C ε (hC e) (hD e)
225 
226 /-- Only the tested chords require defect bounds. Tree-edge errors are not
227 included as hypotheses. -/
228 theorem uniform_chord_bound (T : GraphTree.Rooted α r)
229     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
230     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
231     (U : V r ≃ₗ[ℂ] W r) (C_B ε C_A : ℝ)
232     (hB : ∀ v, ‖(pathL B (GraphTree.rootPath T v)).toContinuousLinearMap‖ ≤ C_B)
233     (hD : ∀ e : GraphTree.Chord T, ‖cycleDefect T A B U e.val.2.2‖ ≤ ε)
234     (hA : ∀ u, ‖(pathL A (GraphTree.rootPath T u)).symm.toContinuousLinearMap‖ ≤ C_A)
235     (e : GraphTree.Chord T) :
236     ‖edgeResidual T A B U e.val.2.2‖ ≤ C_B * ε * C_A :=
237   ContinuousHolonomyResidual.uniform_bound U.toContinuousLinearEquiv
238     (pathL A (GraphTree.rootPath T e.val.1))
239     (pathL A (GraphTree.rootPath T e.val.2.1))
240     (pathL B (GraphTree.rootPath T e.val.1))
241     (pathL B (GraphTree.rootPath T e.val.2.1))
242     (A e.val.2.2).toContinuousLinearEquiv (B e.val.2.2).toContinuousLinearEquiv
243     C_B ε C_A (hB e.val.2.1) (hD e) (hA e.val.1)
244 
245 /-- Chord-only uniform control using the exact mixed path factor. -/
246 theorem uniform_chord_product_bound (T : GraphTree.Rooted α r)
247     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
248     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
249     (U : V r ≃ₗ[ℂ] W r) (C ε : ℝ)
250     (hC : ∀ e : GraphTree.Chord T,
251       ‖(pathL B (GraphTree.rootPath T e.val.2.1)).toContinuousLinearMap‖ *
252         ‖(pathL A (GraphTree.rootPath T e.val.1)).symm.toContinuousLinearMap‖ ≤ C)
253     (hD : ∀ e : GraphTree.Chord T, ‖cycleDefect T A B U e.val.2.2‖ ≤ ε)
254     (e : GraphTree.Chord T) : ‖edgeResidual T A B U e.val.2.2‖ ≤ C * ε :=
255   ContinuousHolonomyResidual.product_conditioning_bound U.toContinuousLinearEquiv
256     (pathL A (GraphTree.rootPath T e.val.1))
257     (pathL A (GraphTree.rootPath T e.val.2.1))
258     (pathL B (GraphTree.rootPath T e.val.1))
259     (pathL B (GraphTree.rootPath T e.val.2.1))
260     (A e.val.2.2).toContinuousLinearEquiv (B e.val.2.2).toContinuousLinearEquiv
261     C ε (hC e) (hD e)
262 
263 /-- Connectedness supplies the tree used in the quantitative statement. -/
264 theorem connected_residual_bound (hc : GraphTree.Connected (α := α))
265     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[ℂ] V v))
266     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[ℂ] W v))
267     (U : V r ≃ₗ[ℂ] W r) {u v : α} (e : u ⟶ v) :
268     let T := GraphTree.ofConnected r hc
269     ‖edgeResidual T A B U e‖ ≤
270       ‖(pathL B (GraphTree.rootPath T v)).toContinuousLinearMap‖ * ‖cycleDefect T A B U e‖ *
271         ‖(pathL A (GraphTree.rootPath T u)).symm.toContinuousLinearMap‖ :=
272   residual_norm_bound (GraphTree.ofConnected r hc) A B U e
273 
274 end PaperXI.GraphResidual

Back to source controls