OverlapPathRepair.lean

1 import KomorebiSpace.OverlapTransport
2 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
3 import Mathlib.Tactic.Linarith
4 import Mathlib.Tactic.NormNum
5 import Mathlib.Tactic.Ring
6 
7 set_option autoImplicit false
8 
9 /-!
10 # A correction from measured overlap paths
11 
12 All edges carry the actual source-frame residual. The correction is a finite
13 sum along specified root paths. Its norm follows from path length, rather
14 than being a right-inverse or spectral-gap assumption.
15 -/
16 universe u v
17 noncomputable section
18 namespace KomorebiSpace
19 namespace OverlapTransport
20 variable {V : Type u} {H : Type v}
21 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
22 abbrev Edges (graph : SimpleGraph V) := {p : V × V // graph.Adj p.1 p.2}
23 noncomputable instance edgesFintype [Fintype V] (graph : SimpleGraph V) :
24     Fintype (Edges graph) := Fintype.ofFinite _
25 structure Routing (graph : SimpleGraph V) (o : V) where
26   path : ∀ i, graph.Walk o i
27   at_anchor : path o = .nil
28 variable (e : Frames (V := V) (H := H)) (graph : SimpleGraph V)
29 def pathIntegral (r : Edges graph → H) : {i j : V} → graph.Walk i j → H
30   | _, _, .nil => 0
31   | i, _, .cons h p => (e i).symm (r ⟨(_, _), h⟩) + pathIntegral r p
32 @[simp] theorem pathIntegral_nil (r : Edges graph → H) (i : V) :
33     pathIntegral e graph r (SimpleGraph.Walk.nil (u := i)) = 0 := rfl
34 theorem pathIntegral_add (r s : Edges graph → H) {i j : V} (p : graph.Walk i j) :
35     pathIntegral e graph (r+s) p = pathIntegral e graph r p + pathIntegral e graph s p := by
36   induction p with
37   | nil => simp [pathIntegral]
38   | cons h p ih => simp only [pathIntegral, Pi.add_apply, map_add, ih]; abel
39 theorem pathIntegral_smul (c : ℝ) (r : Edges graph → H) {i j : V}
40     (p : graph.Walk i j) :
41     pathIntegral e graph (c • r) p = c • pathIntegral e graph r p := by
42   induction p with
43   | nil => simp [pathIntegral]
44   | cons h p ih => simp [pathIntegral, ih, smul_add]
45 variable [Fintype V]
46 def differentialLinear : (V → H) →ₗ[ℝ] (Edges graph → H) where
47   toFun x a := defect e x a.val.1 a.val.2
48   map_add' := by
49     intro x y
50     funext a
51     simp only [defect, Pi.add_apply, map_add]
52     abel
53   map_smul' := by intro c x; funext a; simp [defect, map_smul, smul_sub]
54 theorem differentialLinear_bound (x : V → H) :
55     ‖differentialLinear e graph x‖ ≤ 2 * ‖x‖ := by
56   apply (pi_norm_le_iff_of_nonneg (mul_nonneg (by norm_num) (norm_nonneg x))).mpr
57   intro a
58   change ‖transport e a.val.1 a.val.2 (x a.val.2) - x a.val.1‖ ≤ _
59   calc
60     _ ≤ ‖transport e a.val.1 a.val.2 (x a.val.2)‖ + ‖x a.val.1‖ := norm_sub_le _ _
61     _ = ‖x a.val.2‖ + ‖x a.val.1‖ := by rw [(transport e _ _).norm_map]
62     _ ≤ 2 * ‖x‖ := by
63       have h1 := norm_le_pi_norm x a.val.1
64       have h2 := norm_le_pi_norm x a.val.2
65       linarith
66 def edgeDifferential : (V → H) →L[ℝ] (Edges graph → H) :=
67   (differentialLinear e graph).mkContinuous 2 (differentialLinear_bound e graph)
68 @[simp] theorem edgeDifferential_apply (x : V → H) (a : Edges graph) :
69     edgeDifferential e graph x a = defect e x a.val.1 a.val.2 := rfl
70 theorem edgeDifferential_opNorm : ‖edgeDifferential e graph‖ ≤ 2 := by
71   apply (edgeDifferential e graph).opNorm_le_bound (by norm_num)
72   exact differentialLinear_bound e graph
73 theorem pathIntegral_bound (r : Edges graph → H) {i j : V} (p : graph.Walk i j) :
74     ‖pathIntegral e graph r p‖ ≤ (p.length : ℝ) * ‖r‖ := by
75   induction p with
76   | nil => simp [pathIntegral]
77   | @cons i k j h p ih =>
78     have he : ‖(e i).symm (r ⟨(i,k),h⟩)‖ ≤ ‖r‖ := by
79       simpa only [LinearIsometryEquiv.norm_map] using norm_le_pi_norm r ⟨(i,k),h⟩
80     calc
81       _ ≤ ‖(e i).symm (r ⟨(i,k),h⟩)‖ + ‖pathIntegral e graph r p‖ := norm_add_le _ _
82       _ ≤ ‖r‖ + (p.length : ℝ) * ‖r‖ := add_le_add he ih
83       _ = ((SimpleGraph.Walk.cons h p).length : ℝ) * ‖r‖ := by
84         simp only [SimpleGraph.Walk.length_cons, Nat.cast_add, Nat.cast_one]
85         ring
86 theorem pathIntegral_differential (x : V → H) {i j : V} (p : graph.Walk i j) :
87     pathIntegral e graph (edgeDifferential e graph x) p =
88       normalized e x j - normalized e x i := by
89   induction p with
90   | nil => simp [pathIntegral]
91   | cons h p ih =>
92     simp only [pathIntegral, edgeDifferential_apply, normalized_defect, ih]
93     abel
94 namespace Routing
95 variable {graph} {o : V} (routing : Routing graph o)
96 def radius : ℕ := Finset.univ.sup (fun i => (routing.path i).length)
97 theorem length_le_radius (i : V) : (routing.path i).length ≤ routing.radius := by
98   exact Finset.le_sup (f := fun i => (routing.path i).length) (Finset.mem_univ i)
99 def correctionLinear : (Edges graph → H) →ₗ[ℝ] (V → H) where
100   toFun r i := e i (pathIntegral e graph r (routing.path i))
101   map_add' := by intro r s; funext i; simp [pathIntegral_add, map_add]
102   map_smul' := by intro c r; funext i; simp [pathIntegral_smul, map_smul]
103 theorem correctionLinear_bound (r : Edges graph → H) :
104     ‖routing.correctionLinear e r‖ ≤ (routing.radius : ℝ) * ‖r‖ := by
105   apply (pi_norm_le_iff_of_nonneg (mul_nonneg (Nat.cast_nonneg _) (norm_nonneg r))).mpr
106   intro i
107   change ‖e i (pathIntegral e graph r (routing.path i))‖ ≤ _
108   rw [(e i).norm_map]
109   exact (pathIntegral_bound e graph r (routing.path i)).trans
110     (mul_le_mul_of_nonneg_right (by exact_mod_cast routing.length_le_radius i) (norm_nonneg r))
111 def correction : (Edges graph → H) →L[ℝ] (V → H) :=
112   (routing.correctionLinear e).mkContinuous (routing.radius : ℝ)
113     (routing.correctionLinear_bound e)
114 @[simp] theorem correction_apply (r : Edges graph → H) (i : V) :
115     routing.correction e r i = e i (pathIntegral e graph r (routing.path i)) := rfl
116 theorem correction_bound (r : Edges graph → H) :
117     ‖routing.correction e r‖ ≤ (routing.radius : ℝ) * ‖r‖ :=
118   routing.correctionLinear_bound e r
119 theorem correction_opNorm : ‖routing.correction e‖ ≤ (routing.radius : ℝ) := by
120   apply (routing.correction e).opNorm_le_bound (Nat.cast_nonneg _)
121   exact routing.correction_bound e
122 @[simp] theorem correction_anchor (r : Edges graph → H) :
123     routing.correction e r o = 0 := by
124   simp [correction_apply, routing.at_anchor]
125 theorem correction_differential (x : V → H) :
126     routing.correction e (edgeDifferential e graph x) = x - repair e o x := by
127   funext i
128   simp [correction_apply, pathIntegral_differential, normalized,
129     repair, transport_apply, map_sub]
130 @[simp] theorem differential_repair (x : V → H) :
131     edgeDifferential e graph (repair e o x) = 0 := by
132   funext a
133   exact repair_defect e o x a.val.1 a.val.2
134 /-- Right inversion only on residuals of actual candidates. -/
135 theorem differential_correction_differential (x : V → H) :
136     edgeDifferential e graph (routing.correction e (edgeDifferential e graph x)) =
137       edgeDifferential e graph x := by
138   rw [routing.correction_differential e, map_sub, differential_repair (graph := graph) (o := o) e, sub_zero]
139 theorem repair_error (x : V → H) :
140     ‖x - repair e o x‖ ≤ (routing.radius : ℝ) * ‖edgeDifferential e graph x‖ := by
141   rw [← routing.correction_differential e x]
142   exact routing.correction_bound e _
143 include routing in
144 theorem exact_iff_repair (x : V → H) :
145     edgeDifferential e graph x = 0 ↔ repair e o x = x := by
146   constructor
147   · intro hx
148     have he := routing.correction_differential e x
149     rw [hx, map_zero] at he
150     exact (sub_eq_zero.mp he.symm).symm
151   · intro hx
152     rw [← hx]
153     exact differential_repair (graph := graph) (o := o) e x
154 include routing in
155 theorem unique_exact_repair (x : V → H) :
156     ∃! y : V → H, edgeDifferential e graph y = 0 ∧ y o = x o := by
157   refine ⟨repair e o x, ⟨differential_repair (graph := graph) (o := o) e x, repair_anchor e o x⟩, ?_⟩
158   intro y hy
159   calc
160     y = repair e o y := ((routing.exact_iff_repair e y).mp hy.1).symm
161     _ = repair e o x := by funext i; simp only [repair, hy.2]
162 theorem routes_agree_on_actual_residual (other : Routing graph o) (x : V → H) :
163     routing.correction e (edgeDifferential e graph x) =
164       other.correction e (edgeDifferential e graph x) := by
165   rw [routing.correction_differential e, other.correction_differential e]
166 end Routing
167 end OverlapTransport
168 end KomorebiSpace
169 end

Back to source controls