AmplifiedHolonomy.lean

1 import KomorebiSpace.AmplifiedTransport
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Exact holonomy coordinates for bounded nonisometric transports
7 
8 The fixed-vector classification uses invertibility, not preservation of norms.
9 The resulting equivalence is continuous linear, and is not claimed isometric.
10 -/
11 universe u v
12 noncomputable section
13 namespace KomorebiSpace
14 namespace AmplifiedTransport
15 variable {V : Type u} {H : Type v}
16 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
17 namespace Rooted
18 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
19 variable (p : OverlapTransport.Routing graph o)
20 
21 def frame (i : V) : H ≃L[ℝ] H := (T.walkTransport (p.path i)).symm
22 
23 def reconstruct (z : H) (i : V) : H := frame T p i z
24 
25 @[simp] theorem frame_anchor (z : H) : frame T p o z = z := by
26   simp only [frame, p.at_anchor, Connection.walkTransport]
27   rfl
28 
29 @[simp] theorem reconstruct_anchor (z : H) : reconstruct T p z o = z := frame_anchor T p z
30 
31 def holonomy (a : OverlapTransport.Edges graph) : H ≃L[ℝ] H :=
32   ((frame T p a.val.2).trans (T.transport a.val.1 a.val.2)).trans
33     (frame T p a.val.1).symm
34 
35 @[simp] theorem holonomy_apply (a : OverlapTransport.Edges graph) (z : H) :
36     holonomy T p a z = (frame T p a.val.1).symm
37       (T.transport a.val.1 a.val.2 (frame T p a.val.2 z)) := rfl
38 
39 def fixedSpace : Submodule ℝ H where
40   carrier := {z | ∀ a, holonomy T p a z = z}
41   zero_mem' := by intro a; exact map_zero _
42   add_mem' := by intro x y hx hy a; rw [map_add, hx a, hy a]
43   smul_mem' := by intro c x hx a; rw [map_smul, hx a]
44 
45 @[simp] theorem mem_fixedSpace (z : H) :
46     z ∈ fixedSpace T p ↔ ∀ a, holonomy T p a z = z := Iff.rfl
47 
48 theorem normalized_reconstruction_defect (z : H) (a : OverlapTransport.Edges graph) :
49     (frame T p a.val.1).symm (T.defect (reconstruct T p z) a.val.1 a.val.2) =
50       holonomy T p a z - z := by
51   simp only [Connection.defect, reconstruct, map_sub, holonomy_apply,
52     ContinuousLinearEquiv.symm_apply_apply]
53 
54 theorem reconstruct_parallel_iff (z : H) :
55     T.Parallel graph (reconstruct T p z) ↔ z ∈ fixedSpace T p := by
56   constructor
57   · intro hx a
58     have he := congrArg (frame T p a.val.1).symm (hx _ _ a.property)
59     simpa only [holonomy_apply, reconstruct, ContinuousLinearEquiv.symm_apply_apply] using he
60   · intro hz i j hij
61     have he := hz (⟨(i,j),hij⟩ : OverlapTransport.Edges graph)
62     apply (frame T p i).symm.injective
63     simpa only [holonomy_apply, reconstruct, ContinuousLinearEquiv.symm_apply_apply] using he
64 
65 theorem parallel_reconstruction (x : V → H) (hx : T.Parallel graph x) :
66     reconstruct T p (x o) = x := by
67   funext i
68   have he := T.parallel_walk x hx (p.path i)
69   change (T.walkTransport (p.path i)).symm (x o) = x i
70   rw [← he, ContinuousLinearEquiv.symm_apply_apply]
71 
72 theorem parallel_anchor_fixed (x : V → H) (hx : T.Parallel graph x) :
73     x o ∈ fixedSpace T p := by
74   apply (reconstruct_parallel_iff T p (x o)).mp
75   rw [parallel_reconstruction T p x hx]
76   exact hx
77 
78 include p in
79 theorem parallel_unique {x y : V → H} (hx : T.Parallel graph x)
80     (hy : T.Parallel graph y) (he : x o = y o) : x = y := by
81   rw [← parallel_reconstruction T p x hx, ← parallel_reconstruction T p y hy, he]
82 
83 theorem anchor_extendable_iff (z : H) :
84     (∃ x : V → H, T.Parallel graph x ∧ x o = z) ↔ z ∈ fixedSpace T p := by
85   constructor
86   · rintro ⟨x,hx,hz⟩
87     rw [← hz]
88     exact parallel_anchor_fixed T p x hx
89   · intro hz
90     exact ⟨reconstruct T p z, (reconstruct_parallel_iff T p z).mpr hz,
91       reconstruct_anchor T p z⟩
92 
93 theorem anchor_unique_extension_iff (z : H) :
94     (∃! x : V → H, T.Parallel graph x ∧ x o = z) ↔ z ∈ fixedSpace T p := by
95   constructor
96   · intro h; exact (anchor_extendable_iff T p z).mp h.exists
97   · intro hz
98     refine ⟨reconstruct T p z, ⟨(reconstruct_parallel_iff T p z).mpr hz,
99       reconstruct_anchor T p z⟩, ?_⟩
100     intro y hy
101     exact parallel_unique T p hy.1 ((reconstruct_parallel_iff T p z).mpr hz)
102       (hy.2.trans (reconstruct_anchor T p z).symm)
103 
104 theorem fixedSpace_route_independent (q : OverlapTransport.Routing graph o) :
105     fixedSpace T p = fixedSpace T q := by
106   ext z
107   rw [← anchor_extendable_iff T p z, ← anchor_extendable_iff T q z]
108 
109 theorem reconstruction_route_independent (q : OverlapTransport.Routing graph o)
110     (z : H) (hz : z ∈ fixedSpace T p) :
111     reconstruct T p z = reconstruct T q z := by
112   have hq : z ∈ fixedSpace T q := by rw [← fixedSpace_route_independent T p q]; exact hz
113   exact parallel_unique T p ((reconstruct_parallel_iff T p z).mpr hz)
114     ((reconstruct_parallel_iff T q z).mpr hq)
115     ((reconstruct_anchor T p z).trans (reconstruct_anchor T q z).symm)
116 
117 /-- The finite edge-based operator is transport around a genuine closed walk. -/
118 def edgeLoop (a : OverlapTransport.Edges graph) : graph.Walk o o :=
119   (p.path a.val.1).append (.cons a.property (p.path a.val.2).reverse)
120 
121 theorem holonomy_is_loop (a : OverlapTransport.Edges graph) (z : H) :
122     holonomy T p a z = T.walkTransport (edgeLoop p a) z := by
123   simp only [edgeLoop, Connection.walkTransport_append, Connection.walkTransport_cons,
124     Connection.walkTransport_reverse_eq_symm, holonomy_apply, frame,
125     ContinuousLinearEquiv.symm_symm]
126 
127 /-- Finitely many rooted edge loops detect every closed-walk constraint. -/
128 theorem fixed_iff_all_loops (z : H) :
129     z ∈ fixedSpace T p ↔ ∀ q : graph.Walk o o, T.walkTransport q z = z := by
130   constructor
131   · intro hz q
132     have he := T.parallel_walk (reconstruct T p z)
133       ((reconstruct_parallel_iff T p z).mpr hz) q
134     simpa only [reconstruct_anchor] using he
135   · intro hz a
136     rw [holonomy_is_loop]
137     exact hz (edgeLoop p a)
138 
139 section Finite
140 variable [Fintype V]
141 
142 def parallelSpace : Submodule ℝ (V → H) := (T.differential graph).ker
143 
144 def parameterLinearEquiv : fixedSpace T p ≃ₗ[ℝ] parallelSpace T (graph := graph) where
145   toFun z := ⟨reconstruct T p z.val,
146     (T.parallel_iff_differential_zero _).mp ((reconstruct_parallel_iff T p z.val).mpr z.property)⟩
147   invFun x := ⟨x.val o, parallel_anchor_fixed T p x.val
148     ((T.parallel_iff_differential_zero _).mpr x.property)⟩
149   left_inv := by intro z; apply Subtype.ext; exact reconstruct_anchor T p z.val
150   right_inv := by
151     intro x
152     apply Subtype.ext
153     exact parallel_reconstruction T p x.val
154       ((T.parallel_iff_differential_zero _).mpr x.property)
155   map_add' := by intro z w; apply Subtype.ext; funext i; exact map_add (frame T p i) z.val w.val
156   map_smul' := by intro c z; apply Subtype.ext; funext i; exact map_smul (frame T p i) c z.val
157 
158 /-- Bounded reconstruction with the original vertex maximum norm. -/
159 def reconstructMap : H →L[ℝ] (V → H) :=
160   ContinuousLinearMap.pi fun i => (frame T p i).toContinuousLinearMap
161 
162 omit [Fintype V] in
163 @[simp] theorem reconstructMap_apply (z : H) : reconstructMap T p z = reconstruct T p z := rfl
164 
165 theorem reconstruct_bound (z : H) :
166     ‖reconstruct T p z‖ ≤ ‖reconstructMap T p‖ * ‖z‖ :=
167   (reconstructMap T p).le_opNorm z
168 
169 theorem anchor_lower_bound (z : H) : ‖z‖ ≤ ‖reconstruct T p z‖ := by
170   have he := norm_le_pi_norm (reconstruct T p z) o
171   simpa only [reconstruct_anchor] using he
172 
173 /-- The former isometry is replaced by a bounded linear equivalence. -/
174 def parameterEquiv : fixedSpace T p ≃L[ℝ] parallelSpace T (graph := graph) :=
175   (parameterLinearEquiv T p).toContinuousLinearEquivOfBounds
176     ‖reconstructMap T p‖ 1
177     (fun z => reconstruct_bound T p z.val)
178     (by intro x; change ‖x.val o‖ ≤ 1 * ‖x.val‖; rw [one_mul]; exact norm_le_pi_norm x.val o)
179 
180 @[simp] theorem parameterEquiv_coordinate (z : fixedSpace T p) (i : V) :
181     (parameterEquiv T p z).val i = frame T p i z.val := rfl
182 
183 /-- Reverse routes directly control errors in each destination's norm. -/
184 def routeGain : ℝ := ‖fun i : V => T.walkGain (p.path i).reverse‖
185 
186 theorem routeGain_nonneg : 0 ≤ routeGain T p := norm_nonneg _
187 
188 theorem routeGain_le (i : V) : T.walkGain (p.path i).reverse ≤ routeGain T p := by
189   have h := norm_le_pi_norm (fun i : V => T.walkGain (p.path i).reverse) i
190   simpa only [routeGain, Real.norm_eq_abs, abs_of_nonneg (T.walkGain_nonneg _)] using h
191 
192 theorem anchored_approximation_bound (x : V → H) :
193     ‖x-reconstruct T p (x o)‖ ≤ routeGain T p * ‖T.differential graph x‖ := by
194   apply (pi_norm_le_iff_of_nonneg
195     (mul_nonneg (routeGain_nonneg T p) (norm_nonneg _))).mpr
196   intro i
197   have he := T.walk_error x (p.path i).reverse
198   rw [Connection.walkTransport_reverse_eq_symm, norm_sub_rev] at he
199   exact he.trans (mul_le_mul_of_nonneg_right (routeGain_le T p i) (norm_nonneg _))
200 
201 theorem changed_anchor_error (x : V → H) (z : H) :
202     ‖x-reconstruct T p z‖ ≤ routeGain T p * ‖T.differential graph x‖ +
203       ‖reconstructMap T p‖ * ‖x o-z‖ := by
204   calc
205     _ ≤ ‖x-reconstruct T p (x o)‖ + ‖reconstruct T p (x o)-reconstruct T p z‖ :=
206       norm_sub_le_norm_sub_add_norm_sub _ _ _
207     _ ≤ _ := add_le_add (anchored_approximation_bound T p x) (by
208       have he := (reconstructMap T p).le_opNorm (x o-z)
209       simpa only [map_sub, reconstructMap_apply] using he)
210 
211 end Finite
212 end Rooted
213 end AmplifiedTransport
214 end KomorebiSpace
215 end

Back to source controls