OverlapViewBridge.lean

1 import KomorebiSpace.OverlapPathRepair
2 import KomorebiSpace.SectionObstruction
3 import KomorebiSpace.RepairProjection
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Quantitative overlap repair is an actual ambient realization
9 
10 The complete comparison category has one arrow between each ordered pair of
11 views. A connected measured graph supplies a generating set of comparisons.
12 The coefficient system is explicitly trivialized by the supplied isometries.
13 This is a model-specific quantitative theorem, not a norm on arbitrary stacks.
14 -/
15 universe u v
16 noncomputable section
17 namespace KomorebiSpace
18 namespace OverlapTransport
19 open CategoryTheory
20 variable {V : Type u} {H : Type v}
21 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
22 
23 structure PairView (V : Type u) where
24   point : V
25 
26 instance pairViewCategory : Category (PairView V) where
27   Hom _ _ := PUnit
28   id _ := PUnit.unit
29   comp _ _ := PUnit.unit
30   id_comp := by intros; apply Subsingleton.elim
31   comp_id := by intros; apply Subsingleton.elim
32   assoc := by intros; rfl
33 
34 variable (e : Frames (V := V) (H := H))
35 
36 def viewSystem : AdditiveViewSystem (PairView V) (fun _ => H) where
37   pull := fun {i j} _ => (transport e i.point j.point).toLinearEquiv.toLinearMap.toAddHom
38   pull_id := by intro i x; exact transport_self e i.point x
39   pull_comp := by intro i j k f g x; exact (transport_comp e i.point j.point k.point x).symm
40 
41 def rawViews (x : V → H) : PairView V → H := fun i => x i.point
42 
43 def patch (U : Set V) : Set (PairView V) := {i | i.point ∈ U}
44 
45 /-- Agreement with the old additive view differential, including its sign. -/
46 @[simp] theorem view_differential (x : V → H) (i j : V) :
47     (viewSystem e).differential (rawViews x) ⟨i⟩ ⟨j⟩ PUnit.unit = defect e x i j := rfl
48 
49 def ambientFromSeed (z : H) : (viewSystem e).views.Ambient :=
50   ⟨fun i => e i.point z, by
51     intro i j f
52     change transport e i.point j.point (e j.point z) = e i.point z
53     simp [transport_apply]⟩
54 
55 @[simp] theorem ambientFromSeed_coordinate (z : H) (i : V) :
56     (ambientFromSeed e z).val ⟨i⟩ = e i z := rfl
57 
58 /-- The intended global object is an ordinary vector in the supplied reference space. -/
59 def ambientEquiv (o : V) : (viewSystem e).views.Ambient ≃ H where
60   toFun x := (e o).symm (x.val ⟨o⟩)
61   invFun := ambientFromSeed e
62   left_inv := by
63     intro x
64     apply ViewSystem.Ambient.ext
65     intro i
66     exact x.property i ⟨o⟩ PUnit.unit
67   right_inv := by intro z; simp
68 
69 def repairedAmbient (o : V) (x : V → H) : (viewSystem e).views.Ambient :=
70   ambientFromSeed e (normalized e x o)
71 
72 @[simp] theorem repairedAmbient_coordinate (o : V) (x : V → H) (i : V) :
73     (repairedAmbient e o x).val ⟨i⟩ = repair e o x i := rfl
74 
75 /-- Raw prescribed values must agree when expressed in the common frame. -/
76 def boundaryCompatible (U : Set V) (o : V) (x : V → H) : Prop :=
77   ∀ i ∈ U, normalized e x i = normalized e x o
78 
79 theorem repair_preserves_boundary (U : Set V) (o : V) (x : V → H)
80     (hc : boundaryCompatible e U o x) : ∀ i ∈ U, repair e o x i = x i := by
81   intro i hi
82   apply (e i).symm.injective
83   change normalized e (repair e o x) i = normalized e x i
84   rw [normalized_repair]
85   exact (hc i hi).symm
86 
87 /-- The existing quotient detects precisely incompatible prescribed overlap values. -/
88 theorem obstruction_zero_iff_boundary (U : Set V) (o : V) (ho : o ∈ U) (x : V → H) :
89     ((viewSystem e).problem (patch U)).obstruction (rawViews x) = 0 ↔
90       boundaryCompatible e U o x := by
91   rw [(viewSystem e).obstruction_zero_iff_section]
92   constructor
93   · rintro ⟨s,hs⟩ i hi
94     have h0 := hs ⟨⟨o⟩,ho⟩
95     have h1 := hs ⟨⟨i⟩,hi⟩
96     have he := s.property ⟨i⟩ ⟨o⟩ PUnit.unit
97     change transport e i o (s.val ⟨o⟩) = s.val ⟨i⟩ at he
98     change s.val ⟨o⟩ = x o at h0
99     change s.val ⟨i⟩ = x i at h1
100     rw [h0,h1] at he
101     have hn := congrArg (e i).symm he
102     simpa [transport_apply, normalized] using hn.symm
103   · intro hc
104     refine ⟨repairedAmbient e o x, ?_⟩
105     intro i
106     exact repair_preserves_boundary e U o x hc i.val.point i.property
107 
108 variable [Fintype V]
109 variable {graph : SimpleGraph V} {o : V} (routing : Routing graph o)
110 
111 include routing in
112 /-- Measured edge exactness is exactly ambient coherence on the complete comparison category. -/
113 theorem edge_exact_iff_view_exact (x : V → H) :
114     edgeDifferential e graph x = 0 ↔
115       (viewSystem e).differential (rawViews x) = 0 := by
116   rw [(viewSystem e).differential_zero_iff]
117   constructor
118   · intro hx i j f
119     have he := (routing.exact_iff_repair e x).mp hx
120     have hz := repair_defect e o x i.point j.point
121     rw [he] at hz
122     exact sub_eq_zero.mp hz
123   · intro hx
124     funext a
125     exact sub_eq_zero.mpr (hx ⟨a.val.1⟩ ⟨a.val.2⟩ PUnit.unit)
126 
127 /-- A concrete global section, protected values, and a derived analytic bound together. -/
128 theorem quantitative_realization (U : Set V) (ho : o ∈ U) (x : V → H)
129     (hz : ((viewSystem e).problem (patch U)).obstruction (rawViews x) = 0) :
130     ∃ s : (viewSystem e).views.Ambient,
131       (∀ i ∈ U, s.val ⟨i⟩ = x i) ∧
132       ‖x - (fun i => (show H from s.val ⟨i⟩))‖ ≤ (routing.radius : ℝ) * ‖edgeDifferential e graph x‖ := by
133   have hc := (obstruction_zero_iff_boundary e U o ho x).mp hz
134   refine ⟨repairedAmbient e o x, ?_, ?_⟩
135   · exact repair_preserves_boundary e U o x hc
136   · exact routing.repair_error e x
137 
138 /-- Anchor evaluation as an actual continuous linear protected observable. -/
139 def anchorObservation (o : V) : (V → H) →L[ℝ] H :=
140   (LinearMap.proj o).mkContinuous 1 (by intro x; simpa using norm_le_pi_norm x o)
141 
142 @[simp] theorem anchorObservation_apply (o : V) (x : V → H) :
143     anchorObservation o x = x o := rfl
144 
145 /-- Instantiate the existing correction scheme, with all its obligations derived. -/
146 def Routing.scheme : RepairDynamics.Scheme (edgeDifferential e graph) (anchorObservation o) where
147   correction := routing.correction e
148   rate := 0
149   rate_nonneg := le_rfl
150   rate_lt_one := zero_lt_one
151   preserve := routing.correction_anchor e
152   contract := by
153     intro x
154     rw [routing.differential_correction_differential e x, sub_self, norm_zero, zero_mul]
155 
156 @[simp] theorem scheme_step (x : V → H) :
157     RepairDynamics.step (edgeDifferential e graph) (routing.scheme e).correction x =
158       repair e o x := by
159   change x - routing.correction e (edgeDifferential e graph x) = _
160   rw [routing.correction_differential e]
161   abel
162 
163 variable [CompleteSpace H]
164 
165 /-- The old iterative projector and the explicit overlap repair are the same operator. -/
166 theorem scheme_projection (x : V → H) :
167     (routing.scheme e).projection x = repair e o x := by
168   have hx := (routing.scheme e).limit_exact x
169   have hp := (routing.scheme e).limit_semantics x
170   change (routing.scheme e).limit x = _
171   have he := (routing.exact_iff_repair e _).mp hx
172   calc
173     (routing.scheme e).limit x = repair e o ((routing.scheme e).limit x) := he.symm
174     _ = repair e o x := by
175       funext i
176       change transport e i o ((routing.scheme e).limit x o) = transport e i o (x o)
177       exact congrArg (transport e i o) hp
178 
179 end OverlapTransport
180 end KomorebiSpace
181 end

Back to source controls