RepairProjection.lean

1 import KomorebiSpace.RepairDynamics
2 
3 set_option autoImplicit false
4 
5 /-!
6 # A bounded projection onto exact candidates
7 
8 A fixed bounded correction operator with geometric contraction determines a
9 bounded linear projection onto the exact kernel. Different valid correction
10 operators need not give the same projection without semantic separation.
11 -/
12 universe u v w z
13 noncomputable section
14 namespace KomorebiSpace
15 namespace RepairDynamics
16 open Filter
17 open scoped Topology
18 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
19 variable {E : Type v} {R : Type w} {S : Type z}
20 variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
21 variable [NormedAddCommGroup R] [NormedSpace 𝕜 R]
22 variable [NormedAddCommGroup S] [NormedSpace 𝕜 S]
23 
24 /-- Data sufficient to construct a protected exactification projection. -/
25 structure Scheme (d : E →L[𝕜] R) (p : E →L[𝕜] S) where
26   correction : R →L[𝕜] E
27   rate : ℝ
28   rate_nonneg : 0 ≤ rate
29   rate_lt_one : rate < 1
30   preserve : ∀ r, p (correction r) = 0
31   contract : ∀ x, ‖d x - d (correction (d x))‖ ≤ rate * ‖d x‖
32 
33 theorem orbit_add (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x y : E) (n : ℕ) :
34     orbit d A (x+y) n = orbit d A x n + orbit d A y n := by
35   induction n with
36   | zero => rfl
37   | succ n ih =>
38     simp only [orbit_succ, step, ih, map_add]
39     abel
40 
41 theorem orbit_smul (d : E →L[𝕜] R) (A : R →L[𝕜] E) (c : 𝕜) (x : E) (n : ℕ) :
42     orbit d A (c • x) n = c • orbit d A x n := by
43   induction n with
44   | zero => rfl
45   | succ n ih => simp [orbit_succ, step, ih, smul_sub]
46 
47 variable [CompleteSpace E]
48 namespace Scheme
49 variable {d : E →L[𝕜] R} {p : E →L[𝕜] S} (B : Scheme d p)
50 
51 def limit (x : E) : E :=
52   Classical.choose (exactification_from_correction_operator d p B.correction
53     B.rate B.rate_nonneg B.rate_lt_one B.preserve B.contract x)
54 
55 theorem limit_spec (x : E) :
56     Tendsto (orbit d B.correction x) atTop (𝓝 (B.limit x)) ∧
57       d (B.limit x) = 0 ∧ p (B.limit x) = p x ∧
58       ∀ n, dist (orbit d B.correction x n) (B.limit x) ≤
59         (‖B.correction‖ / (1-B.rate)) * ‖d (orbit d B.correction x n)‖ :=
60   Classical.choose_spec (exactification_from_correction_operator d p B.correction
61     B.rate B.rate_nonneg B.rate_lt_one B.preserve B.contract x)
62 
63 theorem tendsto_limit (x : E) :
64     Tendsto (orbit d B.correction x) atTop (𝓝 (B.limit x)) := (B.limit_spec x).1
65 
66 @[simp] theorem limit_exact (x : E) : d (B.limit x) = 0 := (B.limit_spec x).2.1
67 
68 @[simp] theorem limit_semantics (x : E) : p (B.limit x) = p x :=
69   (B.limit_spec x).2.2.1
70 
71 theorem limit_error (x : E) :
72     dist x (B.limit x) ≤ (‖B.correction‖ / (1-B.rate)) * ‖d x‖ :=
73   (B.limit_spec x).2.2.2 0
74 
75 /-- The limit fixes all exact elements, independently of semantic injectivity. -/
76 theorem limit_fixes_exact (x : E) (hx : d x = 0) : B.limit x = x := by
77   have h : Tendsto (orbit d B.correction x) atTop (𝓝 x) := by
78     change Tendsto (fun n => orbit d B.correction x n) atTop (𝓝 x)
79     simpa only [orbit_fixes_exact d B.correction x hx] using
80       (tendsto_const_nhds : Tendsto (fun _ : ℕ => x) atTop (𝓝 x))
81   exact tendsto_nhds_unique (B.tendsto_limit x) h
82 
83 theorem limit_add (x y : E) : B.limit (x+y) = B.limit x + B.limit y := by
84   have h : Tendsto (orbit d B.correction (x+y)) atTop (𝓝 (B.limit x + B.limit y)) := by
85     change Tendsto (fun n => orbit d B.correction (x+y) n) atTop (𝓝 (B.limit x + B.limit y))
86     simpa only [orbit_add] using (B.tendsto_limit x).add (B.tendsto_limit y)
87   exact tendsto_nhds_unique (B.tendsto_limit (x+y)) h
88 
89 theorem limit_smul (c : 𝕜) (x : E) : B.limit (c • x) = c • B.limit x := by
90   have h : Tendsto (orbit d B.correction (c • x)) atTop (𝓝 (c • B.limit x)) := by
91     change Tendsto (fun n => orbit d B.correction (c • x) n) atTop (𝓝 (c • B.limit x))
92     simpa only [orbit_smul] using (B.tendsto_limit x).const_smul c
93   exact tendsto_nhds_unique (B.tendsto_limit (c • x)) h
94 
95 /-- A supplied correction scheme yields linearity of its limiting repair. -/
96 def linearProjection : E →ₗ[𝕜] E where
97   toFun := B.limit
98   map_add' := B.limit_add
99   map_smul' := B.limit_smul
100 
101 def stabilityConstant : ℝ := 1 + (‖B.correction‖ / (1-B.rate)) * ‖d‖
102 
103 omit [CompleteSpace E] in
104 theorem stabilityConstant_nonneg : 0 ≤ B.stabilityConstant := by
105   have h : 0 < 1-B.rate := sub_pos.mpr B.rate_lt_one
106   unfold stabilityConstant
107   positivity
108 
109 theorem limit_bound (x : E) : ‖B.limit x‖ ≤ B.stabilityConstant * ‖x‖ := by
110   have hC : 0 ≤ ‖B.correction‖ / (1-B.rate) :=
111     div_nonneg (norm_nonneg _) (le_of_lt (sub_pos.mpr B.rate_lt_one))
112   calc
113     ‖B.limit x‖ = dist 0 (B.limit x) := (dist_zero_left _).symm
114     _ ≤ dist 0 x + dist x (B.limit x) := dist_triangle _ _ _
115     _ = ‖x‖ + dist x (B.limit x) := by rw [dist_zero_left]
116     _ ≤ ‖x‖ + (‖B.correction‖ / (1-B.rate)) * ‖d x‖ :=
117       add_le_add le_rfl (B.limit_error x)
118     _ ≤ ‖x‖ + (‖B.correction‖ / (1-B.rate)) * (‖d‖ * ‖x‖) :=
119       add_le_add le_rfl (mul_le_mul_of_nonneg_left (d.le_opNorm x) hC)
120     _ = B.stabilityConstant * ‖x‖ := by unfold stabilityConstant; ring
121 
122 /-- The exactification limit is a constructed bounded linear operator. -/
123 def projection : E →L[𝕜] E :=
124   B.linearProjection.mkContinuous B.stabilityConstant B.limit_bound
125 
126 @[simp] theorem projection_apply (x : E) : B.projection x = B.limit x := rfl
127 
128 theorem projection_bound : ‖B.projection‖ ≤ B.stabilityConstant :=
129   ContinuousLinearMap.opNorm_le_bound _ B.stabilityConstant_nonneg B.limit_bound
130 
131 /-- Idempotence: repeated exactification introduces no further change. -/
132 theorem projection_idempotent (x : E) : B.projection (B.projection x) = B.projection x :=
133   B.limit_fixes_exact _ (B.limit_exact x)
134 
135 /-- The image is exactly the zero-residual kernel. -/
136 theorem projection_image_iff (y : E) : (∃ x, B.projection x = y) ↔ d y = 0 := by
137   constructor
138   · rintro ⟨x, rfl⟩
139     exact B.limit_exact x
140   · intro hy
141     exact ⟨y, B.limit_fixes_exact y hy⟩
142 
143 /-- Every candidate splits into an exact part and a semantically invisible correction. -/
144 theorem exact_residual_splitting (x : E) :
145     x = B.projection x + (x - B.projection x) ∧
146     d (B.projection x) = 0 ∧ p (x - B.projection x) = 0 ∧
147     d (x - B.projection x) = d x ∧ B.projection (x - B.projection x) = 0 := by
148   refine ⟨by abel, B.limit_exact x, ?_, ?_, ?_⟩
149   · simp only [map_sub, projection_apply, limit_semantics, sub_self]
150   · simp only [map_sub, projection_apply, limit_exact, sub_zero]
151   · rw [map_sub, B.projection_idempotent, sub_self]
152 
153 /-- Different valid schemes agree only under the stated separation hypothesis. -/
154 theorem scheme_independent (B' : Scheme d p)
155     (hsep : ∀ a b, d a = 0 → d b = 0 → p a = p b → a = b) :
156     B.projection = B'.projection := by
157   ext x
158   exact hsep _ _ (B.limit_exact x) (B'.limit_exact x)
159     ((B.limit_semantics x).trans (B'.limit_semantics x).symm)
160 
161 end Scheme
162 end RepairDynamics
163 end KomorebiSpace
164 end

Back to source controls