AmplifiedViews.lean

1 import KomorebiSpace.AmplifiedRepair
2 import KomorebiSpace.HolonomyViews
3 import KomorebiSpace.ViewSections
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Nonisometric reconstruction in the existing ambient-section language
9 
10 The graph-walk view category is reused from v0.18. Only its actual transport
11 functor changes. The quantitative statement returns the old Ambient type.
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 abbrev PathView (graph : SimpleGraph V) := HolonomyTransport.PathView graph
21 
22 namespace Connection
23 variable (T : Connection V H) (graph : SimpleGraph V)
24 
25 def pathViews : ViewSystem (PathView graph) where
26   Obj := fun _ => H
27   pull := fun f => T.walkTransport f
28   pull_id := by intros; rfl
29   pull_comp := by intro i j k f g z; exact T.walkTransport_append f g z
30 
31 def ambientValues (x : (T.pathViews graph).Ambient) : V → H := fun i => x.val ⟨i⟩
32 
33 def toAmbient (x : V → H) (hx : T.Parallel graph x) : (T.pathViews graph).Ambient :=
34   ⟨fun i => x i.vertex, fun _i _j f => T.parallel_walk x hx f⟩
35 
36 @[simp] theorem toAmbient_coordinate (x : V → H) (hx : T.Parallel graph x) (i : V) :
37     (T.toAmbient graph x hx).val ⟨i⟩ = x i := rfl
38 
39 theorem ambient_parallel (x : (T.pathViews graph).Ambient) :
40     T.Parallel graph (fun i => x.val ⟨i⟩) := by
41   intro i j hij
42   exact x.property ⟨i⟩ ⟨j⟩ (.cons hij .nil)
43 
44 /-- This is the old Ambient type with the new, actual walk restriction maps. -/
45 def ambientParallelEquiv :
46     (T.pathViews graph).Ambient ≃ {x : V → H // T.Parallel graph x} where
47   toFun x := ⟨fun i => x.val ⟨i⟩, T.ambient_parallel graph x⟩
48   invFun x := T.toAmbient graph x.val x.property
49   left_inv := by intro x; apply ViewSystem.Ambient.ext; intro i; rfl
50   right_inv := by intro x; rfl
51 
52 end Connection
53 
54 namespace Rooted
55 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
56 variable (p : OverlapTransport.Routing graph o)
57 
58 def ambientParameters : fixedSpace T p ≃ (T.pathViews graph).Ambient where
59   toFun z := T.toAmbient graph (reconstruct T p z.val)
60     ((reconstruct_parallel_iff T p z.val).mpr z.property)
61   invFun x := ⟨x.val ⟨o⟩, parallel_anchor_fixed T p (fun i => x.val ⟨i⟩)
62     (T.ambient_parallel graph x)⟩
63   left_inv := by intro z; apply Subtype.ext; exact reconstruct_anchor T p z.val
64   right_inv := by
65     intro x
66     apply ViewSystem.Ambient.ext
67     intro i
68     exact congrFun (parallel_reconstruction T p (fun j => x.val ⟨j⟩)
69       (T.ambient_parallel graph x)) i.vertex
70 
71 @[simp] theorem ambientParameters_coordinate (z : fixedSpace T p) (i : V) :
72     (ambientParameters T p z).val ⟨i⟩ = frame T p i z.val := rfl
73 
74 section Finite
75 variable [Fintype V]
76 
77 theorem quantitative_ambient_realization (U : Set V) (ho : o ∈ U) (x : V → H)
78     (hx : (problem T (graph := graph) U).obstruction x = 0) :
79     ∃ s : (T.pathViews graph).Ambient,
80       (∀ i : U, s.val ⟨i.val⟩ = x i.val) ∧
81       ‖x - T.ambientValues graph s‖ ≤ routeGain T p * ‖T.differential graph x‖ := by
82   obtain ⟨y,hy,_⟩ := quantitative_prescribed_repair T p U ho x hx
83   exact ⟨T.toAmbient graph y hy.1, hy.2.1, hy.2.2⟩
84 
85 end Finite
86 end Rooted
87 end AmplifiedTransport
88 end KomorebiSpace
89 end
90 
91 noncomputable section
92 namespace KomorebiSpace
93 namespace AmplifiedTransport
94 namespace Rooted
95 variable {V : Type u} {H : Type v}
96 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H] [Fintype V]
97 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
98 variable (p : OverlapTransport.Routing graph o)
99 
100 def orthogonalAmbient (x : V → H) : (T.pathViews graph).Ambient :=
101   T.toAmbient graph (orthogonalRepair T p x) (orthogonalRepair_parallel T p x)
102 
103 theorem finite_dimensional_ambient_repair (x : V → H) :
104     ∃ s : (T.pathViews graph).Ambient,
105       anchorProjection T p (s.val ⟨o⟩) = anchorProjection T p (x o) ∧
106       ‖x-T.ambientValues graph s‖ ≤ stabilityGain T p * ‖T.differential graph x‖ := by
107   refine ⟨orthogonalAmbient T p x, ?_, orthogonalRepair_error T p x⟩
108   change anchorProjection T p (orthogonalRepair T p x o) = _
109   rw [orthogonalRepair_anchor, anchorProjection_idempotent]
110 
111 end Rooted
112 end AmplifiedTransport
113 end KomorebiSpace
114 end

Back to source controls