OverlapResidualImage.lean

1 import KomorebiSpace.OverlapPathRepair
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Which independently supplied edge residuals are integrable?
7 
8 The route operator projects edge data onto the image of the actual overlap
9 operator. It is not a right inverse on arbitrary residuals. An antisymmetric
10 triangle example violates loop consistency and has no primitive.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace OverlapTransport
16 variable {V : Type u} {H : Type v}
17 variable [NormedAddCommGroup H] [NormedSpace ℝ H] [Fintype V]
18 variable (e : Frames (V := V) (H := H))
19 variable {graph : SimpleGraph V} {o : V}
20 
21 /-- Actual overlap defects have zero normalized circulation on every closed walk. -/
22 theorem actual_closed_walk (x : V → H) (i : V) (p : graph.Walk i i) :
23     pathIntegral e graph (edgeDifferential e graph x) p = 0 := by
24   rw [pathIntegral_differential, sub_self]
25 
26 namespace Routing
27 variable (routing : Routing graph o)
28 
29 def residualProjection : (Edges graph → H) →L[ℝ] (Edges graph → H) :=
30   (edgeDifferential e graph).comp (routing.correction e)
31 
32 @[simp] theorem residualProjection_apply (r : Edges graph → H) :
33     routing.residualProjection e r = edgeDifferential e graph (routing.correction e r) := rfl
34 
35 @[simp] theorem residualProjection_actual (x : V → H) :
36     routing.residualProjection e (edgeDifferential e graph x) = edgeDifferential e graph x :=
37   routing.differential_correction_differential e x
38 
39 theorem residualProjection_idempotent (r : Edges graph → H) :
40     routing.residualProjection e (routing.residualProjection e r) = routing.residualProjection e r := by
41   exact routing.differential_correction_differential e (routing.correction e r)
42 
43 def routeObstruction : (Edges graph → H) →L[ℝ] (Edges graph → H) :=
44   ContinuousLinearMap.id ℝ _ - routing.residualProjection e
45 
46 @[simp] theorem routeObstruction_apply (r : Edges graph → H) :
47     routing.routeObstruction e r = r - routing.residualProjection e r := rfl
48 
49 /-- The diagnostic vanishes exactly for the actual image, not for every edge family. -/
50 theorem routeObstruction_zero_iff (r : Edges graph → H) :
51     routing.routeObstruction e r = 0 ↔ ∃ x : V → H, edgeDifferential e graph x = r := by
52   constructor
53   · intro h
54     refine ⟨routing.correction e r, ?_⟩
55     exact (sub_eq_zero.mp h).symm
56   · rintro ⟨x,rfl⟩
57     rw [routeObstruction_apply, residualProjection_apply,
58       routing.differential_correction_differential e x, sub_self]
59 
60 theorem routeObstruction_idempotent (r : Edges graph → H) :
61     routing.routeObstruction e (routing.routeObstruction e r) = routing.routeObstruction e r := by
62   simp only [routeObstruction_apply, map_sub, routing.residualProjection_idempotent e,
63     sub_self, sub_zero]
64 
65 theorem repair_correction (r : Edges graph → H) :
66     repair e o (routing.correction e r) = 0 := by
67   funext i
68   simp [repair, routing.correction_anchor e]
69 
70 /-- The nonintegrable remainder contributes nothing to the selected route primitive. -/
71 theorem correction_obstruction_zero (r : Edges graph → H) :
72     routing.correction e (routing.routeObstruction e r) = 0 := by
73   rw [routeObstruction_apply, map_sub, residualProjection_apply,
74     routing.correction_differential e, routing.repair_correction e, sub_zero, sub_self]
75 
76 theorem routeObstruction_bound (r : Edges graph → H) :
77     ‖routing.routeObstruction e r‖ ≤ (1 + 2 * (routing.radius : ℝ)) * ‖r‖ := by
78   have hd := differentialLinear_bound e graph (routing.correction e r)
79   have ha := routing.correction_bound e r
80   calc
81     _ ≤ ‖r‖ + ‖routing.residualProjection e r‖ := norm_sub_le _ _
82     _ ≤ ‖r‖ + 2 * (routing.radius : ℝ) * ‖r‖ := by
83       change ‖r‖ + ‖differentialLinear e graph (routing.correction e r)‖ ≤ _
84       nlinarith
85     _ = _ := by ring
86 
87 end Routing
88 
89 namespace CycleBoundary
90 
91 def triangleFrames : Frames (V := Fin 3) (H := ℝ) := fun _ => LinearIsometryEquiv.refl ℝ ℝ
92 
93 def triangleResidual : Edges (⊤ : SimpleGraph (Fin 3)) → ℝ := fun a =>
94   if (a.val.1 = 0 ∧ a.val.2 = 1) ∨ (a.val.1 = 1 ∧ a.val.2 = 2) then 1
95   else if (a.val.1 = 1 ∧ a.val.2 = 0) ∨ (a.val.1 = 2 ∧ a.val.2 = 1) then -1 else 0
96 
97 /-- Even an antisymmetric edge assignment need not be the disagreement of vertex data. -/
98 theorem triangle_no_primitive :
99     ¬ ∃ x : Fin 3 → ℝ, edgeDifferential triangleFrames ⊤ x = triangleResidual := by
100   rintro ⟨x,hx⟩
101   let a01 : Edges (⊤ : SimpleGraph (Fin 3)) := ⟨(0,1), by simp⟩
102   let a12 : Edges (⊤ : SimpleGraph (Fin 3)) := ⟨(1,2), by simp⟩
103   let a02 : Edges (⊤ : SimpleGraph (Fin 3)) := ⟨(0,2), by simp⟩
104   have h01 := congrFun hx a01
105   have h12 := congrFun hx a12
106   have h02 := congrFun hx a02
107   change x 1 - x 0 = 1 at h01
108   change x 2 - x 1 = 1 at h12
109   change x 2 - x 0 = 0 at h02
110   linarith
111 
112 end CycleBoundary
113 end OverlapTransport
114 end KomorebiSpace
115 end

Back to source controls