OverlapTransport.lean

1 import Mathlib.Analysis.Normed.Operator.LinearIsometry
2 import Mathlib.Analysis.Normed.Group.Constructions
3 import Mathlib.Analysis.Normed.Operator.NormedSpace
4 import Mathlib.Tactic.Abel
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Flat isometric overlap data and anchored repair
10 
11 The supplied frames define actual overlap maps. Their existence is an explicit
12 model hypothesis, not asserted for arbitrary local systems. The repair below
13 is constructed, not assumed as a right inverse or a spectral estimate.
14 -/
15 universe u v
16 noncomputable section
17 namespace KomorebiSpace
18 namespace OverlapTransport
19 variable {V : Type u} {H : Type v}
20 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
21 abbrev Frames := V → H ≃ₗᵢ[ℝ] H
22 variable (e : Frames (V := V) (H := H))
23 def normalized (x : V → H) (i : V) : H := (e i).symm (x i)
24 def transport (i j : V) : H ≃ₗᵢ[ℝ] H := (e j).symm.trans (e i)
25 @[simp] theorem transport_apply (i j : V) (z : H) :
26     transport e i j z = e i ((e j).symm z) := rfl
27 @[simp] theorem transport_self (i : V) (z : H) : transport e i i z = z := by
28   simp [transport_apply]
29 theorem transport_comp (i j k : V) (z : H) :
30     transport e i j (transport e j k z) = transport e i k z := by
31   simp [transport_apply]
32 /-- The residual has the same orientation as the existing view differential. -/
33 def defect (x : V → H) (i j : V) : H := transport e i j (x j) - x i
34 @[simp] theorem normalized_defect (x : V → H) (i j : V) :
35     (e i).symm (defect e x i j) = normalized e x j - normalized e x i := by
36   simp [defect, transport_apply, normalized, map_sub]
37 theorem norm_defect (x : V → H) (i j : V) :
38     ‖defect e x i j‖ = ‖normalized e x j - normalized e x i‖ := by
39   rw [← normalized_defect e x i j]
40   exact ((e i).symm.norm_map _).symm
41 theorem defect_comp (x : V → H) (i j k : V) :
42     defect e x i k = defect e x i j + transport e i j (defect e x j k) := by
43   simp [defect, transport_apply, map_sub]
44 /-- The whole vector at the anchor is protected. -/
45 def repair (o : V) (x : V → H) (i : V) : H := transport e i o (x o)
46 @[simp] theorem repair_anchor (o : V) (x : V → H) : repair e o x o = x o := by
47   simp [repair]
48 @[simp] theorem repair_defect (o : V) (x : V → H) (i j : V) :
49     defect e (repair e o x) i j = 0 := by
50   simp [defect, repair]
51 @[simp] theorem repair_idempotent (o : V) (x : V → H) :
52     repair e o (repair e o x) = repair e o x := by
53   funext i
54   simp [repair]
55 theorem normalized_repair (o : V) (x : V → H) (i : V) :
56     normalized e (repair e o x) i = normalized e x o := by
57   simp [normalized, repair, transport_apply]
58 theorem repair_error_coordinate (o : V) (x : V → H) (i : V) :
59     ‖x i - repair e o x i‖ = ‖normalized e x i - normalized e x o‖ := by
60   rw [← (e i).symm.norm_map (x i - repair e o x i), map_sub]
61   rw [show (e i).symm (repair e o x i) = normalized e x o from
62     normalized_repair e o x i]
63   rfl
64 theorem repair_fixes (o : V) (x : V → H)
65     (hx : ∀ i j, defect e x i j = 0) : repair e o x = x := by
66   funext i
67   exact sub_eq_zero.mp (hx i o)
68 theorem unique_repair (o : V) (x : V → H) :
69     ∃! y : V → H, (∀ i j, defect e y i j = 0) ∧ y o = x o := by
70   refine ⟨repair e o x, ⟨repair_defect e o x, repair_anchor e o x⟩, ?_⟩
71   intro y hy
72   funext i
73   have he := sub_eq_zero.mp (hy.1 i o)
74   rw [hy.2] at he
75   exact he.symm
76 section Finite
77 variable [Fintype V]
78 def repairLinear (o : V) : (V → H) →ₗ[ℝ] (V → H) where
79   toFun := repair e o
80   map_add' := by intro x y; funext i; simp [repair, map_add]
81   map_smul' := by intro c x; funext i; simp [repair, map_smul]
82 theorem repair_bound (o : V) (x : V → H) : ‖repair e o x‖ ≤ ‖x‖ := by
83   apply (pi_norm_le_iff_of_nonneg (norm_nonneg x)).mpr
84   intro i
85   simpa [repair] using norm_le_pi_norm x o
86 def repairCLM (o : V) : (V → H) →L[ℝ] (V → H) :=
87   (repairLinear e o).mkContinuous 1 (by
88     intro x
89     change ‖repair e o x‖ ≤ 1 * ‖x‖
90     simpa using repair_bound e o x)
91 @[simp] theorem repairCLM_apply (o : V) (x : V → H) :
92     repairCLM e o x = repair e o x := rfl
93 theorem repair_opNorm (o : V) : ‖repairCLM e o‖ ≤ 1 := by
94   apply (repairCLM e o).opNorm_le_bound zero_le_one
95   intro x
96   simpa using repair_bound e o x
97 theorem repair_stability (o : V) (x y : V → H) :
98     ‖repair e o x - repair e o y‖ ≤ ‖x-y‖ := by
99   change ‖repairCLM e o x - repairCLM e o y‖ ≤ _
100   rw [← map_sub]
101   exact repair_bound e o (x-y)
102 end Finite
103 
104 def reframe (a : Frames (V := V) (H := H)) : Frames (V := V) (H := H) :=
105   fun i => (e i).trans (a i)
106 def changeValues (a : Frames (V := V) (H := H)) (x : V → H) : V → H :=
107   fun i => a i (x i)
108 theorem reframe_normalized (a : Frames (V := V) (H := H)) (x : V → H) (i : V) :
109     normalized (reframe e a) (changeValues a x) i = normalized e x i := by
110   simp [normalized, reframe, changeValues]
111 theorem reframe_defect (a : Frames (V := V) (H := H)) (x : V → H) (i j : V) :
112     defect (reframe e a) (changeValues a x) i j = a i (defect e x i j) := by
113   simp [defect, transport_apply, reframe, changeValues, map_sub]
114 theorem reframe_defect_norm (a : Frames (V := V) (H := H)) (x : V → H) (i j : V) :
115     ‖defect (reframe e a) (changeValues a x) i j‖ = ‖defect e x i j‖ := by
116   rw [reframe_defect]
117   exact (a i).norm_map _
118 theorem reframe_repair (a : Frames (V := V) (H := H)) (o : V) (x : V → H) :
119     repair (reframe e a) o (changeValues a x) = changeValues a (repair e o x) := by
120   funext i
121   simp [repair, transport_apply, reframe, changeValues]
122 end OverlapTransport
123 end KomorebiSpace
124 end

Back to source controls