HolonomyCoordinates.lean

1 import KomorebiSpace.HolonomyTransport
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Exact realizations are fixed anchor vectors
7 
8 Root routes construct frames; they are not assumed to trivialize the connection.
9 Every edge then defines a loop operator at the anchor. The common fixed space
10 classifies exactly the parallel sections, with norm and anchor preserved.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace HolonomyTransport
16 variable {V : Type u} {H : Type v}
17 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
18 namespace Rooted
19 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
20 variable (p : OverlapTransport.Routing graph o)
21 
22 def frame (i : V) : H ≃ₗᵢ[ℝ] H := (T.walkTransport (p.path i)).symm
23 
24 def reconstruct (z : H) (i : V) : H := frame T p i z
25 
26 @[simp] theorem frame_anchor (z : H) : frame T p o z = z := by
27   simp only [frame, p.at_anchor, Connection.walkTransport]
28   rfl
29 
30 @[simp] theorem reconstruct_anchor (z : H) : reconstruct T p z o = z := frame_anchor T p z
31 
32 def holonomy (a : OverlapTransport.Edges graph) : H ≃ₗᵢ[ℝ] H :=
33   ((frame T p a.val.2).trans (T.transport a.val.1 a.val.2)).trans
34     (frame T p a.val.1).symm
35 
36 @[simp] theorem holonomy_apply (a : OverlapTransport.Edges graph) (z : H) :
37     holonomy T p a z = (frame T p a.val.1).symm
38       (T.transport a.val.1 a.val.2 (frame T p a.val.2 z)) := rfl
39 
40 def fixedSpace : Submodule ℝ H where
41   carrier := {z | ∀ a, holonomy T p a z = z}
42   zero_mem' := by intro a; exact map_zero _
43   add_mem' := by intro x y hx hy a; rw [map_add, hx a, hy a]
44   smul_mem' := by intro c x hx a; rw [map_smul, hx a]
45 
46 @[simp] theorem mem_fixedSpace (z : H) :
47     z ∈ fixedSpace T p ↔ ∀ a, holonomy T p a z = z := Iff.rfl
48 
49 theorem normalized_reconstruction_defect (z : H) (a : OverlapTransport.Edges graph) :
50     (frame T p a.val.1).symm (T.defect (reconstruct T p z) a.val.1 a.val.2) =
51       holonomy T p a z - z := by
52   simp only [Connection.defect, reconstruct, map_sub, holonomy_apply,
53     LinearIsometryEquiv.symm_apply_apply]
54 
55 theorem reconstruct_parallel_iff (z : H) :
56     T.Parallel graph (reconstruct T p z) ↔ z ∈ fixedSpace T p := by
57   constructor
58   · intro hx a
59     have he := congrArg (frame T p a.val.1).symm (hx _ _ a.property)
60     simpa only [holonomy_apply, reconstruct, LinearIsometryEquiv.symm_apply_apply] using he
61   · intro hz i j hij
62     have he := hz (⟨(i,j),hij⟩ : OverlapTransport.Edges graph)
63     apply (frame T p i).symm.injective
64     simpa only [holonomy_apply, reconstruct, LinearIsometryEquiv.symm_apply_apply] using he
65 
66 theorem parallel_reconstruction (x : V → H) (hx : T.Parallel graph x) :
67     reconstruct T p (x o) = x := by
68   funext i
69   have he := T.parallel_walk x hx (p.path i)
70   change (T.walkTransport (p.path i)).symm (x o) = x i
71   rw [← he, LinearIsometryEquiv.symm_apply_apply]
72 
73 theorem parallel_anchor_fixed (x : V → H) (hx : T.Parallel graph x) :
74     x o ∈ fixedSpace T p := by
75   apply (reconstruct_parallel_iff T p (x o)).mp
76   rw [parallel_reconstruction T p x hx]
77   exact hx
78 
79 include p in
80 theorem parallel_unique {x y : V → H} (hx : T.Parallel graph x)
81     (hy : T.Parallel graph y) (he : x o = y o) : x = y := by
82   rw [← parallel_reconstruction T p x hx, ← parallel_reconstruction T p y hy, he]
83 
84 theorem anchor_extendable_iff (z : H) :
85     (∃ x : V → H, T.Parallel graph x ∧ x o = z) ↔ z ∈ fixedSpace T p := by
86   constructor
87   · rintro ⟨x,hx,hz⟩
88     rw [← hz]
89     exact parallel_anchor_fixed T p x hx
90   · intro hz
91     exact ⟨reconstruct T p z, (reconstruct_parallel_iff T p z).mpr hz,
92       reconstruct_anchor T p z⟩
93 
94 theorem anchor_unique_extension_iff (z : H) :
95     (∃! x : V → H, T.Parallel graph x ∧ x o = z) ↔ z ∈ fixedSpace T p := by
96   constructor
97   · intro h; exact (anchor_extendable_iff T p z).mp h.exists
98   · intro hz
99     refine ⟨reconstruct T p z, ⟨(reconstruct_parallel_iff T p z).mpr hz,
100       reconstruct_anchor T p z⟩, ?_⟩
101     intro y hy
102     exact parallel_unique T p hy.1 ((reconstruct_parallel_iff T p z).mpr hz)
103       (hy.2.trans (reconstruct_anchor T p z).symm)
104 
105 theorem fixedSpace_route_independent (q : OverlapTransport.Routing graph o) :
106     fixedSpace T p = fixedSpace T q := by
107   ext z
108   rw [← anchor_extendable_iff T p z, ← anchor_extendable_iff T q z]
109 
110 theorem reconstruction_route_independent (q : OverlapTransport.Routing graph o)
111     (z : H) (hz : z ∈ fixedSpace T p) :
112     reconstruct T p z = reconstruct T q z := by
113   have hq : z ∈ fixedSpace T q := by rw [← fixedSpace_route_independent T p q]; exact hz
114   exact parallel_unique T p ((reconstruct_parallel_iff T p z).mpr hz)
115     ((reconstruct_parallel_iff T q z).mpr hq)
116     ((reconstruct_anchor T p z).trans (reconstruct_anchor T q z).symm)
117 
118 /-- The finite edge-based operator is transport around a genuine closed walk. -/
119 def edgeLoop (a : OverlapTransport.Edges graph) : graph.Walk o o :=
120   (p.path a.val.1).append (.cons a.property (p.path a.val.2).reverse)
121 
122 theorem holonomy_is_loop (a : OverlapTransport.Edges graph) (z : H) :
123     holonomy T p a z = T.walkTransport (edgeLoop p a) z := by
124   simp only [edgeLoop, Connection.walkTransport_append, Connection.walkTransport_cons,
125     Connection.walkTransport_reverse_eq_symm, holonomy_apply, frame,
126     LinearIsometryEquiv.symm_symm]
127 
128 /-- Finitely many rooted edge loops detect every closed-walk constraint. -/
129 theorem fixed_iff_all_loops (z : H) :
130     z ∈ fixedSpace T p ↔ ∀ q : graph.Walk o o, T.walkTransport q z = z := by
131   constructor
132   · intro hz q
133     have he := T.parallel_walk (reconstruct T p z)
134       ((reconstruct_parallel_iff T p z).mpr hz) q
135     simpa only [reconstruct_anchor] using he
136   · intro hz a
137     rw [holonomy_is_loop]
138     exact hz (edgeLoop p a)
139 
140 section Finite
141 variable [Fintype V]
142 
143 def parallelSpace : Submodule ℝ (V → H) := (T.differential graph).ker
144 
145 def parameterLinearEquiv : fixedSpace T p ≃ₗ[ℝ] parallelSpace T (graph := graph) where
146   toFun z := ⟨reconstruct T p z.val,
147     (T.parallel_iff_differential_zero _).mp ((reconstruct_parallel_iff T p z.val).mpr z.property)⟩
148   invFun x := ⟨x.val o, parallel_anchor_fixed T p x.val
149     ((T.parallel_iff_differential_zero _).mpr x.property)⟩
150   left_inv := by intro z; apply Subtype.ext; exact reconstruct_anchor T p z.val
151   right_inv := by
152     intro x
153     apply Subtype.ext
154     exact parallel_reconstruction T p x.val
155       ((T.parallel_iff_differential_zero _).mpr x.property)
156   map_add' := by intro z w; apply Subtype.ext; funext i; exact map_add (frame T p i) z.val w.val
157   map_smul' := by intro c z; apply Subtype.ext; funext i; exact map_smul (frame T p i) c z.val
158 
159 theorem reconstruct_norm (z : H) : ‖reconstruct T p z‖ = ‖z‖ := by
160   apply le_antisymm
161   · apply (pi_norm_le_iff_of_nonneg (norm_nonneg z)).mpr
162     intro i
163     exact le_of_eq ((frame T p i).norm_map z)
164   · have he := norm_le_pi_norm (reconstruct T p z) o
165     simpa only [reconstruct_anchor] using he
166 
167 /-- An actual linear isometric equivalence, not only a dimension count. -/
168 def parameterEquiv : fixedSpace T p ≃ₗᵢ[ℝ] parallelSpace T (graph := graph) where
169   toLinearEquiv := parameterLinearEquiv T p
170   norm_map' := by intro z; exact reconstruct_norm T p z.val
171 
172 @[simp] theorem parameterEquiv_coordinate (z : fixedSpace T p) (i : V) :
173     (parameterEquiv T p z).val i = frame T p i z.val := rfl
174 
175 /-- Routed reconstruction is close to a candidate, even when its anchor is inadmissible. -/
176 theorem anchored_approximation_bound (x : V → H) :
177     ‖x - reconstruct T p (x o)‖ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ := by
178   apply (pi_norm_le_iff_of_nonneg
179     (mul_nonneg (Nat.cast_nonneg _) (norm_nonneg _))).mpr
180   intro i
181   have he : ‖x i - reconstruct T p (x o) i‖ =
182       ‖T.walkTransport (p.path i) (x i) - x o‖ := by
183     rw [← (T.walkTransport (p.path i)).norm_map, map_sub]
184     simp only [reconstruct, frame, LinearIsometryEquiv.apply_symm_apply]
185   rw [show (x - reconstruct T p (x o)) i = x i - reconstruct T p (x o) i from rfl, he]
186   exact (T.walk_error x (p.path i)).trans
187     (mul_le_mul_of_nonneg_right (by exact_mod_cast p.length_le_radius i) (norm_nonneg _))
188 
189 /-- Feasible anchors admit the same graph-derived error bound as in the flat model. -/
190 theorem anchored_quantitative_repair (x : V → H) (hx : x o ∈ fixedSpace T p) :
191     ∃! y : V → H, T.Parallel graph y ∧ y o = x o ∧
192       ‖x-y‖ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ := by
193   refine ⟨reconstruct T p (x o), ⟨(reconstruct_parallel_iff T p _).mpr hx,
194     reconstruct_anchor T p _, anchored_approximation_bound T p x⟩, ?_⟩
195   intro y hy
196   exact parallel_unique T p hy.1 ((reconstruct_parallel_iff T p _).mpr hx)
197     (hy.2.1.trans (reconstruct_anchor T p _).symm)
198 
199 end Finite
200 end Rooted
201 end HolonomyTransport
202 end KomorebiSpace
203 end

Back to source controls