AmplifiedTransport.lean

1 import KomorebiSpace.HolonomyTransport
2 import Mathlib.Combinatorics.SimpleGraph.Walk.Operations
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Bounded invertible transports and actual path amplification
8 
9 Each edge is a continuous linear equivalence, not assumed isometric or flat.
10 Walk products retain their order. The error estimate is derived from the
11 transported residual sum and recursive operator-norm gain.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace AmplifiedTransport
17 variable {V : Type u} {H : Type v}
18 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
19 
20 structure Connection (V : Type u) (H : Type v)
21     [NormedAddCommGroup H] [NormedSpace ℝ H] where
22   transport : V → V → H ≃L[ℝ] H
23   self_apply : ∀ i z, transport i i z = z
24   reverse_apply : ∀ i j z, transport i j (transport j i z) = z
25 
26 namespace Connection
27 variable (T : Connection V H) {graph : SimpleGraph V}
28 
29 /-- The older isometric connection is embedded without changing its edge maps. -/
30 def ofIsometric (T : HolonomyTransport.Connection V H) : Connection V H where
31   transport i j := (T.transport i j).toContinuousLinearEquiv
32   self_apply := T.self_apply
33   reverse_apply := T.reverse_apply
34 
35 /-- A flat subclass with arbitrary bounded invertible local frames. -/
36 def ofFrames (e : V → H ≃L[ℝ] H) : Connection V H where
37   transport i j := (e j).symm.trans (e i)
38   self_apply := by intro i z; exact (e i).apply_symm_apply z
39   reverse_apply := by
40     intro i j z
41     change e i ((e j).symm (e j ((e i).symm z))) = z
42     rw [ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.apply_symm_apply]
43 
44 def defect (x : V → H) (i j : V) : H := T.transport i j (x j) - x i
45 
46 def Parallel (graph : SimpleGraph V) (x : V → H) : Prop :=
47   ∀ i j, graph.Adj i j → T.transport i j (x j) = x i
48 
49 def walkTransport : {i j : V} → graph.Walk i j → H ≃L[ℝ] H
50   | _, _, .nil => ContinuousLinearEquiv.refl ℝ H
51   | i, _, @SimpleGraph.Walk.cons _ _ _ j _ _ p =>
52       (walkTransport p).trans (T.transport i j)
53 
54 @[simp] theorem walkTransport_nil (i : V) (z : H) :
55     T.walkTransport (SimpleGraph.Walk.nil (G := graph) (u := i)) z = z := rfl
56 
57 @[simp] theorem walkTransport_cons {i j k : V} (h : graph.Adj i j)
58     (p : graph.Walk j k) (z : H) :
59     T.walkTransport (.cons h p) z = T.transport i j (T.walkTransport p z) := rfl
60 
61 theorem walkTransport_append {i j k : V} (p : graph.Walk i j)
62     (q : graph.Walk j k) (z : H) :
63     T.walkTransport (p.append q) z = T.walkTransport p (T.walkTransport q z) := by
64   induction p with
65   | nil => rfl
66   | @cons i j k h p ih =>
67     simpa only [SimpleGraph.Walk.cons_append, walkTransport_cons] using
68       congrArg (T.transport i j) (ih q)
69 
70 /-- Reverse edge consistency supplies inverse transport along every reversed walk. -/
71 theorem walkTransport_reverse {i j : V} (p : graph.Walk i j) (z : H) :
72     T.walkTransport p.reverse (T.walkTransport p z) = z := by
73   induction p with
74   | nil => rfl
75   | @cons i k j h p ih =>
76     rw [SimpleGraph.Walk.reverse_cons,
77       walkTransport_append, walkTransport_cons, walkTransport_nil, walkTransport_cons,
78       T.reverse_apply]
79     exact ih
80 
81 theorem walkTransport_reverse_eq_symm {i j : V} (p : graph.Walk i j) (z : H) :
82     T.walkTransport p.reverse z = (T.walkTransport p).symm z := by
83   have he := T.walkTransport_reverse p ((T.walkTransport p).symm z)
84   simpa only [ContinuousLinearEquiv.apply_symm_apply] using he
85 
86 theorem parallel_walk (x : V → H) (hx : T.Parallel graph x)
87     {i j : V} (p : graph.Walk i j) : T.walkTransport p (x j) = x i := by
88   induction p with
89   | nil => rfl
90   | cons h p ih => rw [walkTransport_cons, ih, hx _ _ h]
91 
92 theorem parallel_iff_all_walks (x : V → H) :
93     T.Parallel graph x ↔ ∀ i j (p : graph.Walk i j), T.walkTransport p (x j) = x i := by
94   constructor
95   · intro hx i j p; exact T.parallel_walk x hx p
96   · intro hx i j h
97     exact hx i j (.cons h .nil)
98 
99 /-- A path gain: one direct edge defect plus amplified later defects. -/
100 def walkGain : {i j : V} → graph.Walk i j → ℝ
101   | _, _, .nil => 0
102   | i, _, @SimpleGraph.Walk.cons _ _ _ j _ _ p =>
103       1 + ‖(T.transport i j).toContinuousLinearMap‖ * walkGain p
104 
105 @[simp] theorem walkGain_nil (i : V) :
106     T.walkGain (SimpleGraph.Walk.nil (G := graph) (u := i)) = 0 := rfl
107 
108 @[simp] theorem walkGain_cons {i j k : V} (h : graph.Adj i j)
109     (p : graph.Walk j k) : T.walkGain (.cons h p) =
110       1 + ‖(T.transport i j).toContinuousLinearMap‖ * T.walkGain p := rfl
111 
112 theorem walkGain_nonneg {i j : V} (p : graph.Walk i j) : 0 ≤ T.walkGain p := by
113   induction p with
114   | nil => exact le_rfl
115   | cons h p ih =>
116     rw [walkGain_cons]
117     exact add_nonneg zero_le_one (mul_nonneg (norm_nonneg _) ih)
118 
119 /-- Product of the edge norm bounds in their original path order. -/
120 def walkProduct : {i j : V} → graph.Walk i j → ℝ
121   | _, _, .nil => 1
122   | i, _, @SimpleGraph.Walk.cons _ _ _ j _ _ p =>
123       ‖(T.transport i j).toContinuousLinearMap‖ * walkProduct p
124 
125 theorem walkGain_append {i j k : V} (p : graph.Walk i j) (q : graph.Walk j k) :
126     T.walkGain (p.append q) = T.walkGain p + T.walkProduct p * T.walkGain q := by
127   induction p with
128   | nil => simp [walkGain, walkProduct]
129   | @cons i j k h p ih =>
130     simp only [SimpleGraph.Walk.cons_append, walkGain_cons, walkProduct, ih]
131     ring
132 
133 theorem walkGain_le_length (hc : ∀ i j, graph.Adj i j →
134     ‖(T.transport i j).toContinuousLinearMap‖ ≤ 1)
135     {i j : V} (p : graph.Walk i j) : T.walkGain p ≤ (p.length : ℝ) := by
136   induction p with
137   | nil => simp
138   | @cons i k j h p ih =>
139     rw [walkGain_cons, SimpleGraph.Walk.length_cons, Nat.cast_add, Nat.cast_one]
140     have hm := mul_le_mul_of_nonneg_right (hc i k h) (T.walkGain_nonneg p)
141     rw [one_mul] at hm
142     linarith
143 
144 /-- A quantitative residual sum, with each term expressed in the starting fiber. -/
145 def walkSum (r : OverlapTransport.Edges graph → H) :
146     {i j : V} → graph.Walk i j → H
147   | _, _, .nil => 0
148   | i, _, @SimpleGraph.Walk.cons _ _ _ j _ h p =>
149       r ⟨(i,j),h⟩ + T.transport i j (walkSum r p)
150 
151 theorem walkSum_defect (x : V → H) {i j : V} (p : graph.Walk i j) :
152     T.walkSum (fun a => T.defect x a.val.1 a.val.2) p =
153       T.walkTransport p (x j) - x i := by
154   induction p with
155   | nil => simp [walkSum]
156   | @cons i k j h p ih =>
157     change T.defect x i k + T.transport i k (T.walkSum _ p) = _
158     rw [ih, map_sub, walkTransport_cons]
159     unfold defect
160     abel
161 
162 section Finite
163 variable [Fintype V]
164 abbrev Edges (graph : SimpleGraph V) := OverlapTransport.Edges graph
165 
166 /-- Only measured edges determine this finite bound. -/
167 def edgeBound (graph : SimpleGraph V) : ℝ :=
168   ‖fun a : Edges graph => (T.transport a.val.1 a.val.2).toContinuousLinearMap‖
169 
170 theorem edgeBound_nonneg (graph : SimpleGraph V) : 0 ≤ T.edgeBound graph := norm_nonneg _
171 
172 def differentialLinear (graph : SimpleGraph V) : (V → H) →ₗ[ℝ] (Edges graph → H) where
173   toFun x a := T.defect x a.val.1 a.val.2
174   map_add' := by
175     intro x y
176     funext a
177     simp only [defect, Pi.add_apply, map_add]
178     abel
179   map_smul' := by
180     intro c x
181     funext a
182     simp [defect, map_smul, smul_sub]
183 
184 theorem differentialLinear_bound (graph : SimpleGraph V) (x : V → H) :
185     ‖T.differentialLinear graph x‖ ≤ (T.edgeBound graph + 1) * ‖x‖ := by
186   apply (pi_norm_le_iff_of_nonneg
187     (mul_nonneg (add_nonneg (T.edgeBound_nonneg graph) zero_le_one) (norm_nonneg _))).mpr
188   intro a
189   change ‖T.transport a.val.1 a.val.2 (x a.val.2) - x a.val.1‖ ≤ _
190   have hm : ‖(T.transport a.val.1 a.val.2).toContinuousLinearMap‖ ≤ T.edgeBound graph :=
191     norm_le_pi_norm (fun a : Edges graph => (T.transport a.val.1 a.val.2).toContinuousLinearMap) a
192   calc
193     _ ≤ ‖T.transport a.val.1 a.val.2 (x a.val.2)‖ + ‖x a.val.1‖ := norm_sub_le _ _
194     _ ≤ ‖(T.transport a.val.1 a.val.2).toContinuousLinearMap‖ * ‖x a.val.2‖ + ‖x a.val.1‖ :=
195       add_le_add ((T.transport a.val.1 a.val.2).toContinuousLinearMap.le_opNorm _) le_rfl
196     _ ≤ T.edgeBound graph * ‖x‖ + ‖x‖ :=
197       add_le_add (mul_le_mul hm (norm_le_pi_norm x a.val.2) (norm_nonneg _)
198         (T.edgeBound_nonneg graph)) (norm_le_pi_norm x a.val.1)
199     _ = _ := by ring
200 
201 def differential (graph : SimpleGraph V) : (V → H) →L[ℝ] (Edges graph → H) :=
202   (T.differentialLinear graph).mkContinuous (T.edgeBound graph + 1)
203     (T.differentialLinear_bound graph)
204 
205 @[simp] theorem differential_apply (x : V → H) (a : Edges graph) :
206     T.differential graph x a = T.defect x a.val.1 a.val.2 := rfl
207 
208 theorem differential_bound (graph : SimpleGraph V) (x : V → H) :
209     ‖T.differential graph x‖ ≤ (T.edgeBound graph + 1) * ‖x‖ :=
210   T.differentialLinear_bound graph x
211 
212 theorem differential_opNorm (graph : SimpleGraph V) :
213     ‖T.differential graph‖ ≤ T.edgeBound graph + 1 := by
214   apply ContinuousLinearMap.opNorm_le_bound _ (add_nonneg (T.edgeBound_nonneg graph) zero_le_one)
215   exact T.differential_bound graph
216 
217 theorem parallel_iff_differential_zero (x : V → H) :
218     T.Parallel graph x ↔ T.differential graph x = 0 := by
219   constructor
220   · intro hx; funext a; exact sub_eq_zero.mpr (hx _ _ a.property)
221   · intro hx i j h
222     exact sub_eq_zero.mp (congrFun hx (⟨(i,j),h⟩ : Edges graph))
223 
224 theorem walkSum_bound (r : Edges graph → H) {i j : V} (p : graph.Walk i j) :
225     ‖T.walkSum r p‖ ≤ T.walkGain p * ‖r‖ := by
226   induction p with
227   | nil => simp [walkSum]
228   | @cons i k j h p ih =>
229     change ‖r ⟨(i,k),h⟩ + T.transport i k (T.walkSum r p)‖ ≤ _
230     calc
231       _ ≤ ‖r ⟨(i,k),h⟩‖ + ‖T.transport i k (T.walkSum r p)‖ := norm_add_le _ _
232       _ ≤ ‖r‖ + ‖(T.transport i k).toContinuousLinearMap‖ * ‖T.walkSum r p‖ :=
233         add_le_add (norm_le_pi_norm r ⟨(i,k),h⟩)
234           ((T.transport i k).toContinuousLinearMap.le_opNorm _)
235       _ ≤ ‖r‖ + ‖(T.transport i k).toContinuousLinearMap‖ * (T.walkGain p * ‖r‖) :=
236         add_le_add le_rfl (mul_le_mul_of_nonneg_left ih (norm_nonneg _))
237       _ = _ := by rw [walkGain_cons]; ring
238 
239 theorem walk_error (x : V → H) {i j : V} (p : graph.Walk i j) :
240     ‖T.walkTransport p (x j) - x i‖ ≤ T.walkGain p * ‖T.differential graph x‖ := by
241   rw [← T.walkSum_defect x p]
242   exact T.walkSum_bound (T.differential graph x) p
243 
244 @[simp] theorem ofIsometric_differential (S : HolonomyTransport.Connection V H)
245     (x : V → H) : (ofIsometric S).differential graph x = S.differential graph x := rfl
246 
247 end Finite
248 end Connection
249 end AmplifiedTransport
250 end KomorebiSpace
251 end

Back to source controls