SplitTowerSemantics.lean

1 import KomorebiSpace.SplitTowerRepair
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Protected seed and innovation coordinates
7 
8 A target splitting distinguishes inherited output from the new output kernel.
9 The full observable protects the initial operator and every innovation row.
10 Unlike evaluation at level zero alone, this observable separates exact maps.
11 All canonicity statements remain relative to the specified splitting.
12 -/
13 universe u v
14 noncomputable section
15 open scoped NNReal ENNReal
16 namespace KomorebiSpace
17 namespace BanachTower
18 namespace Splitting
19 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
20 variable (X : BanachTower.{u,v} 𝕜) {Y : BanachTower.{u,v} 𝕜}
21 variable (L : Splitting Y)
22 
23 /-- The output component not inherited through the chosen target section. -/
24 def innovation (f : Candidates X Y) (n : ℕ) : X.Obj (n+1) →L[𝕜] Y.Obj (n+1) :=
25   f (n+1) - (L.up n).comp ((Y.down n).comp (f (n+1)))
26 
27 theorem innovation_bound (f : Candidates X Y) (n : ℕ) :
28     ‖L.innovation X f n‖ ≤ (1 + (L.bound : ℝ) * Y.bound) * ‖f‖ := by
29   have hf := lp.norm_apply_le_norm ENNReal.top_ne_zero f (n+1)
30   have hd : ‖(Y.down n).comp (f (n+1))‖ ≤ (Y.bound : ℝ) * ‖f‖ :=
31     ((Y.down n).opNorm_comp_le _).trans
32       (mul_le_mul (Y.down_bound n) hf (norm_nonneg _) (NNReal.coe_nonneg _))
33   have hu : ‖(L.up n).comp ((Y.down n).comp (f (n+1)))‖ ≤
34       (L.bound : ℝ) * ((Y.bound : ℝ) * ‖f‖) :=
35     ((L.up n).opNorm_comp_le _).trans
36       (mul_le_mul (L.up_bound n) hd (norm_nonneg _) (NNReal.coe_nonneg _))
37   calc
38     ‖L.innovation X f n‖ ≤ ‖f (n+1)‖ +
39         ‖(L.up n).comp ((Y.down n).comp (f (n+1)))‖ := norm_sub_le _ _
40     _ ≤ ‖f‖ + (L.bound : ℝ) * ((Y.bound : ℝ) * ‖f‖) := add_le_add hf hu
41     _ = (1 + (L.bound : ℝ) * Y.bound) * ‖f‖ := by ring
42 
43 def rawObservable (f : Candidates X Y) : ∀ n, X.Obj n →L[𝕜] Y.Obj n
44   | 0 => f 0
45   | n+1 => L.innovation X f n
46 
47 theorem rawObservable_bound (f : Candidates X Y) (n : ℕ) :
48     ‖L.rawObservable X f n‖ ≤ (1 + (L.bound : ℝ) * Y.bound) * ‖f‖ := by
49   cases n with
50   | zero =>
51     have hf := lp.norm_apply_le_norm ENNReal.top_ne_zero f 0
52     have ht : 0 ≤ (L.bound : ℝ) * (Y.bound : ℝ) :=
53       mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _)
54     change ‖f 0‖ ≤ _
55     nlinarith [norm_nonneg f]
56   | succ n => exact L.innovation_bound X f n
57 
58 def observableLinear : Candidates X Y →ₗ[𝕜] Candidates X Y where
59   toFun f := ⟨L.rawObservable X f, memℓp_infty ⟨(1 + (L.bound : ℝ) * Y.bound) * ‖f‖,
60     by rintro _ ⟨n, rfl⟩; exact L.rawObservable_bound X f n⟩⟩
61   map_add' f g := by
62     apply lp.ext
63     funext n
64     cases n with
65     | zero => rfl
66     | succ n =>
67       ext x
68       simp only [rawObservable, innovation, lp.coeFn_add, Pi.add_apply,
69         ContinuousLinearMap.comp_apply, add_apply, sub_apply, map_add]
70       abel
71   map_smul' c f := by
72     apply lp.ext
73     funext n
74     cases n with
75     | zero => rfl
76     | succ n =>
77       ext x
78       simp [rawObservable, innovation, smul_sub]
79 
80 theorem observableLinear_bound (f : Candidates X Y) :
81     ‖L.observableLinear X f‖ ≤ (1 + (L.bound : ℝ) * Y.bound) * ‖f‖ := by
82   apply lp.norm_le_of_forall_le (by positivity)
83   exact L.rawObservable_bound X f
84 
85 /-- A bounded observable retaining all fresh output information, not only the seed. -/
86 def observable : Candidates X Y →L[𝕜] Candidates X Y :=
87   (L.observableLinear X).mkContinuous (1 + (L.bound : ℝ) * Y.bound)
88     (L.observableLinear_bound X)
89 
90 @[simp] theorem observable_zero (f : Candidates X Y) : L.observable X f 0 = f 0 := rfl
91 
92 @[simp] theorem observable_succ (f : Candidates X Y) (n : ℕ) :
93     L.observable X f (n+1) = L.innovation X f n := rfl
94 
95 theorem observable_bound (f : Candidates X Y) :
96     ‖L.observable X f‖ ≤ (1 + (L.bound : ℝ) * Y.bound) * ‖f‖ :=
97   L.observableLinear_bound X f
98 
99 theorem observable_opNorm : ‖L.observable X‖ ≤ 1 + (L.bound : ℝ) * Y.bound :=
100   ContinuousLinearMap.opNorm_le_bound _ (by positivity) (L.observable_bound X)
101 
102 /-- Innovations really take values in the kernel of the target coarse-graining map. -/
103 @[simp] theorem innovation_down (f : Candidates X Y) (n : ℕ) :
104     (Y.down n).comp (L.innovation X f n) = 0 := by
105   ext x
106   simp [innovation]
107 
108 @[simp] theorem observable_idempotent (f : Candidates X Y) :
109     L.observable X (L.observable X f) = L.observable X f := by
110   apply lp.ext
111   funext n
112   cases n with
113   | zero => rfl
114   | succ n =>
115     change L.innovation X (L.observable X f) n = L.innovation X f n
116     ext x
117     simp [innovation]
118 
119 /-- Exact compatibility determines the inherited part at the next level. -/
120 theorem exact_reconstruction (f : Candidates X Y) (hf : Exact X Y f) (n : ℕ) :
121     f (n+1) = (L.up n).comp ((f n).comp (X.down n)) + L.innovation X f n := by
122   rw [← hf n]
123   unfold innovation
124   abel
125 
126 /-- Seed plus innovations, in contrast to the seed alone, distinguish exact maps. -/
127 theorem exact_eq_of_observable (f g : Candidates X Y)
128     (hf : Exact X Y f) (hg : Exact X Y g)
129     (hp : L.observable X f = L.observable X g) : f = g := by
130   apply lp.ext
131   funext n
132   induction n with
133   | zero => simpa only [observable_zero] using
134       congrArg (fun a : Candidates X Y => a 0) hp
135   | succ n ih =>
136     have hn : L.innovation X f n = L.innovation X g n :=
137       congrArg (fun a : Candidates X Y => a (n+1)) hp
138     rw [L.exact_reconstruction X f hf n, L.exact_reconstruction X g hg n, ih, hn]
139 
140 /-- Residual and observable together are injective coordinates on all candidates. -/
141 theorem residual_observable_injective (f g : Candidates X Y)
142     (hd : differential X Y f = differential X Y g)
143     (hp : L.observable X f = L.observable X g) : f = g := by
144   have he : Exact X Y (f-g) := (exact_iff_differential_zero X Y _).mpr (by
145     simp only [map_sub, hd, sub_self])
146   have hz : Exact X Y (0 : Candidates X Y) :=
147     (exact_iff_differential_zero X Y _).mpr (map_zero _)
148   have hh : L.observable X (f-g) = L.observable X 0 := by
149     simp only [map_sub, hp, sub_self, map_zero]
150   exact sub_eq_zero.mp (L.exact_eq_of_observable X (f-g) 0 he hz hh)
151 
152 variable (hgap : (L.bound : ℝ) * X.bound < 1)
153 
154 @[simp] theorem innovation_correction (r : Residuals X Y) (n : ℕ) :
155     L.innovation X (L.correction X hgap r) n = 0 := by
156   ext x
157   simp [innovation, rawCorrection_succ]
158 
159 @[simp] theorem observable_correction (r : Residuals X Y) :
160     L.observable X (L.correction X hgap r) = 0 := by
161   apply lp.ext
162   funext n
163   cases n with
164   | zero => rfl
165   | succ n => exact L.innovation_correction X hgap r n
166 
167 @[simp] theorem repair_preserves_observable (f : Candidates X Y) :
168     L.observable X (L.repair X hgap f) = L.observable X f := by
169   simp only [repair_apply, map_sub, observable_correction, sub_zero]
170 
171 /-- All hypotheses, including semantic separation, are now derived from split towers. -/
172 def fullScheme : RepairDynamics.Scheme (differential X Y) (L.observable X) where
173   correction := L.correction X hgap
174   rate := 0
175   rate_nonneg := le_rfl
176   rate_lt_one := zero_lt_one
177   preserve := L.observable_correction X hgap
178   contract f := by simp
179 
180 include hgap in
181 /-- Existence and uniqueness of exact repair with the full innovation profile fixed. -/
182 theorem unique_exact_repair (f : Candidates X Y) :
183     ∃! g : Candidates X Y, Exact X Y g ∧ L.observable X g = L.observable X f := by
184   refine ⟨L.repair X hgap f,
185     ⟨L.repair_exact X hgap f, L.repair_preserves_observable X hgap f⟩, ?_⟩
186   intro g hg
187   exact L.exact_eq_of_observable X g (L.repair X hgap f) hg.1
188     (L.repair_exact X hgap f)
189     (hg.2.trans (L.repair_preserves_observable X hgap f).symm)
190 
191 /-- Any valid repair engine for this same observable has the explicit projection. -/
192 theorem any_scheme_projection_eq
193     (B : RepairDynamics.Scheme (differential X Y) (L.observable X)) :
194     B.projection = L.repair X hgap := by
195   apply ContinuousLinearMap.ext
196   intro f
197   exact L.exact_eq_of_observable X (B.projection f) (L.repair X hgap f)
198     ((exact_iff_differential_zero X Y _).mpr (B.limit_exact f))
199     (L.repair_exact X hgap f)
200     ((B.limit_semantics f).trans (L.repair_preserves_observable X hgap f).symm)
201 
202 include hgap in
203 /-- Every admissible semantic coordinate and every bounded residual have one candidate. -/
204 theorem unique_candidate_of_coordinates (s : Candidates X Y)
205     (hs : L.observable X s = s) (r : Residuals X Y) :
206     ∃! f : Candidates X Y, differential X Y f = r ∧ L.observable X f = s := by
207   refine ⟨L.repair X hgap s + L.correction X hgap r, ?_, ?_⟩
208   · constructor
209     · simp only [map_add, repair_differential_zero, differential_correction, zero_add]
210     · simp only [map_add, repair_preserves_observable, observable_correction, add_zero, hs]
211   · intro f hf
212     apply L.residual_observable_injective X
213     · simpa only [map_add, repair_differential_zero, differential_correction, zero_add] using hf.1
214     · simpa only [map_add, repair_preserves_observable, observable_correction, add_zero, hs] using hf.2
215 
216 end Splitting
217 end BanachTower
218 end KomorebiSpace
219 end

Back to source controls