HolonomyRepair.lean

1 import KomorebiSpace.HolonomyCoordinates
2 import KomorebiSpace.Correction
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Holonomy-sensitive quantitative repair with protected observations
8 
9 A feasible anchor has a unique parallel extension and a graph-derived bound.
10 The feasibility test is identified with the existing correction quotient.
11 For arbitrary anchors, a separate anchor correction estimate is necessary.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace HolonomyTransport
17 variable {V : Type u} {H : Type v}
18 variable [NormedAddCommGroup H] [NormedSpace ℝ H] [Fintype V]
19 namespace Rooted
20 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
21 variable (p : OverlapTransport.Routing graph o)
22 
23 def rootResidual (z : H) (a : OverlapTransport.Edges graph) : H := holonomy T p a z - z
24 
25 omit [Fintype V] in
26 @[simp] theorem rootResidual_zero_iff (z : H) :
27     rootResidual T p z = 0 ↔ z ∈ fixedSpace T p := by
28   constructor
29   · intro hz a; exact sub_eq_zero.mp (congrFun hz a)
30   · intro hz; funext a; exact sub_eq_zero.mpr (hz a)
31 
32 theorem rootResidual_coordinate_norm (z : H) (a : OverlapTransport.Edges graph) :
33     ‖rootResidual T p z a‖ = ‖T.differential graph (reconstruct T p z) a‖ := by
34   change ‖holonomy T p a z - z‖ = ‖T.defect (reconstruct T p z) a.val.1 a.val.2‖
35   rw [← normalized_reconstruction_defect]
36   exact (frame T p a.val.1).symm.norm_map _
37 
38 theorem rootResidual_norm (z : H) :
39     ‖rootResidual T p z‖ = ‖T.differential graph (reconstruct T p z)‖ := by
40   apply le_antisymm
41   · apply (pi_norm_le_iff_of_nonneg (norm_nonneg _)).mpr
42     intro a
43     rw [rootResidual_coordinate_norm]
44     exact norm_le_pi_norm _ a
45   · apply (pi_norm_le_iff_of_nonneg (norm_nonneg _)).mpr
46     intro a
47     rw [← rootResidual_coordinate_norm]
48     exact norm_le_pi_norm _ a
49 
50 theorem reconstruct_difference_norm (z w : H) :
51     ‖reconstruct T p z - reconstruct T p w‖ = ‖z-w‖ := by
52   have he : reconstruct T p z - reconstruct T p w = reconstruct T p (z-w) := by
53     funext i
54     exact (map_sub (frame T p i) z w).symm
55   rw [he, reconstruct_norm]
56 
57 /-- Small edge residual controls the loop inconsistency of the observed anchor. -/
58 theorem rootResidual_anchor_bound (x : V → H) :
59     ‖rootResidual T p (x o)‖ ≤ (2 * (p.radius : ℝ) + 1) * ‖T.differential graph x‖ := by
60   rw [rootResidual_norm]
61   have ht : ‖T.differential graph (reconstruct T p (x o))‖ ≤
62       ‖T.differential graph (reconstruct T p (x o) - x)‖ + ‖T.differential graph x‖ := by
63     calc
64       _ = ‖T.differential graph (reconstruct T p (x o) - x) + T.differential graph x‖ := by
65         rw [map_sub, sub_add_cancel]
66       _ ≤ _ := norm_add_le _ _
67   have hd := T.differentialLinear_bound graph (reconstruct T p (x o)-x)
68   have he := anchored_approximation_bound T p x
69   change ‖T.differential graph (reconstruct T p (x o)-x)‖ ≤ 2 * ‖reconstruct T p (x o)-x‖ at hd
70   rw [norm_sub_rev] at hd
71   calc
72     _ ≤ 2 * ‖x-reconstruct T p (x o)‖ + ‖T.differential graph x‖ :=
73       by linarith
74     _ ≤ 2 * ((p.radius : ℝ) * ‖T.differential graph x‖) + ‖T.differential graph x‖ :=
75       by linarith
76     _ = _ := by ring
77 
78 theorem changed_anchor_error (x : V → H) (z : H) :
79     ‖x-reconstruct T p z‖ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ + ‖x o-z‖ := by
80   calc
81     _ ≤ ‖x-reconstruct T p (x o)‖ +
82       ‖reconstruct T p (x o)-reconstruct T p z‖ := norm_sub_le_norm_sub_add_norm_sub _ _ _
83     _ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ + ‖x o-z‖ :=
84       add_le_add (anchored_approximation_bound T p x) (le_of_eq (reconstruct_difference_norm T p _ _))
85 
86 /-- A conditional anchor estimate is kept separate from graph propagation. -/
87 theorem repair_from_anchor_estimate (q : H → H) (K : ℝ) (hK : 0 ≤ K)
88     (hq : ∀ z, q z ∈ fixedSpace T p)
89     (hb : ∀ z, ‖z-q z‖ ≤ K * ‖rootResidual T p z‖) (x : V → H) :
90     T.Parallel graph (reconstruct T p (q (x o))) ∧
91       ‖x-reconstruct T p (q (x o))‖ ≤
92         ((p.radius : ℝ) + K * (2 * (p.radius : ℝ)+1)) * ‖T.differential graph x‖ := by
93   constructor
94   · exact (reconstruct_parallel_iff T p _).mpr (hq _)
95   · calc
96       _ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ + ‖x o-q (x o)‖ :=
97         changed_anchor_error T p x _
98       _ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ + K * ‖rootResidual T p (x o)‖ :=
99         by linarith [hb (x o)]
100       _ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ +
101           K * ((2 * (p.radius : ℝ)+1) * ‖T.differential graph x‖) :=
102         by
103           have hm := mul_le_mul_of_nonneg_left (rootResidual_anchor_bound T p x) hK
104           linarith
105       _ = _ := by ring
106 
107 /-- Prescribed vertex values, not only their norms. -/
108 def observation (U : Set V) : (V → H) →+ (U → H) where
109   toFun x i := x i.val
110   map_zero' := rfl
111   map_add' := by intros; rfl
112 
113 def problem (U : Set V) :
114     CorrectionProblem (V → H) (OverlapTransport.Edges graph → H) (U → H) where
115   residual := (T.differential graph).toLinearMap.toAddMonoidHom
116   semantics := observation U
117 
118 /-- The independently defined quotient detects both loop feasibility and prescribed values. -/
119 theorem obstruction_criterion (U : Set V) (ho : o ∈ U) (x : V → H) :
120     (problem T (graph := graph) U).obstruction x = 0 ↔
121       x o ∈ fixedSpace T p ∧ ∀ i : U, reconstruct T p (x o) i.val = x i.val := by
122   rw [CorrectionProblem.flatten_iff]
123   change (∃ y : V → H, T.differential graph y = 0 ∧ observation U y = observation U x) ↔ _
124   constructor
125   · rintro ⟨y,hy,hobs⟩
126     have hp := (T.parallel_iff_differential_zero y).mpr hy
127     have ha : y o = x o := congrFun hobs ⟨o,ho⟩
128     have hr : reconstruct T p (x o) = y := by rw [← ha]; exact parallel_reconstruction T p y hp
129     constructor
130     · rw [← ha]; exact parallel_anchor_fixed T p y hp
131     · intro i; rw [hr]; exact congrFun hobs i
132   · rintro ⟨hx,hU⟩
133     exact ⟨reconstruct T p (x o),
134       (T.parallel_iff_differential_zero _).mp ((reconstruct_parallel_iff T p _).mpr hx),
135       funext hU⟩
136 
137 /-- A nonflat protected reconstruction theorem using the original correction quotient. -/
138 theorem quantitative_prescribed_repair (U : Set V) (ho : o ∈ U) (x : V → H)
139     (hx : (problem T (graph := graph) U).obstruction x = 0) :
140     ∃! y : V → H, T.Parallel graph y ∧ (∀ i : U, y i.val = x i.val) ∧
141       ‖x-y‖ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ := by
142   obtain ⟨hfix,hU⟩ := (obstruction_criterion T p U ho x).mp hx
143   refine ⟨reconstruct T p (x o), ⟨(reconstruct_parallel_iff T p _).mpr hfix,
144     hU, anchored_approximation_bound T p x⟩, ?_⟩
145   intro y hy
146   exact parallel_unique T p hy.1 ((reconstruct_parallel_iff T p _).mpr hfix)
147     ((hy.2.1 ⟨o,ho⟩).trans (reconstruct_anchor T p _).symm)
148 
149 end Rooted
150 end HolonomyTransport
151 end KomorebiSpace
152 end

Back to source controls