LearnedRealization.lean

1 import KomorebiLSM.DelayClosure
2 import KomorebiLSM.IdentificationBound
3 import KomorebiLSM.Realization
4 import KomorebiLSM.DefectPropagation
5 
6 /-! P25: learning from a covering observation table, and explicit rollout bounds. -/
7 set_option autoImplicit false
8 open scoped BigOperators
9 namespace Komorebi.LSM.Identification
10 variable {E V : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
11 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V]
12 variable [FiniteDimensional ℝ E]
13 
14 /-- Depends only on the paired observed columns. -/
15 noncomputable def learned (Zminus Zplus : E →ₗ[ℝ] V) : V →ₗ[ℝ] V :=
16   Zplus.comp (pinv Zminus)
17 
18 theorem learned_eq_true (Zminus Zplus : E →ₗ[ℝ] V) (D : V →ₗ[ℝ] V)
19     (coverage : Function.Surjective Zminus) (successors : Zplus = D.comp Zminus) :
20     learned Zminus Zplus = D := by
21   apply LinearMap.ext
22   intro v
23   obtain ⟨x,rfl⟩ := coverage v
24   change Zplus (pinv Zminus (Zminus x)) = D (Zminus x)
25   rw [successors]
26   change D (Zminus (pinv Zminus (Zminus x))) = _
27   rw [pinv_apply_image, apply_retained]
28 
29 theorem learned_all_horizons (Zminus Zplus : E →ₗ[ℝ] V) (D : V →ₗ[ℝ] V)
30     (coverage : Function.Surjective Zminus) (successors : Zplus = D.comp Zminus)
31     (v : V) (t : ℕ) : (learned Zminus Zplus ^ t) v = (D^t) v := by
32   rw [learned_eq_true Zminus Zplus D coverage successors]
33 
34 /-- Complete packet synthesis preserves every learned state, hence every decoded output. -/
35 theorem learned_packet_output {I O : Type*} [Fintype I] (P : I → V →ₗ[ℝ] V)
36     (complete : ∑ i, P i = LinearMap.id) (H : V → O)
37     (Zminus Zplus : E →ₗ[ℝ] V) (D : V →ₗ[ℝ] V)
38     (coverage : Function.Surjective Zminus) (successors : Zplus = D.comp Zminus)
39     (v : V) (t : ℕ) : H (∑ i, P i ((learned Zminus Zplus ^ t) v)) = H ((D^t) v) := by
40   rw [learned_all_horizons Zminus Zplus D coverage successors]
41   have he := congrArg (fun F : V →ₗ[ℝ] V => F ((D^t) v)) complete
42   simpa only [LinearMap.sum_apply, LinearMap.id_apply] using congrArg H he
43 
44 /-- The same learned transition in a lossless chart has exactly the same iterates. -/
45 theorem learned_atlas_iterates {C : Type*} (a : Realization V C)
46     (Zminus Zplus : E →ₗ[ℝ] V) (D : V →ₗ[ℝ] V)
47     (coverage : Function.Surjective Zminus) (successors : Zplus = D.comp Zminus)
48     (v : V) (t : ℕ) :
49     (Realization.realize a (learned Zminus Zplus) )^[t] (a.encode v) = a.encode ((D^t) v) := by
50   rw [learned_eq_true Zminus Zplus D coverage successors]
51   induction t with
52   | zero => rfl
53   | succ t ih =>
54     rw [Function.iterate_succ_apply', ih]
55     simp only [Realization.realize, Realization.decode_encode, pow_succ', Module.End.mul_apply]
56 
57 /-- Combining P14 with a surjective table on its actual range identifies the delay transition. -/
58 theorem delay_table_identifies {X Y S : Type*} [AddCommGroup X] [Module ℝ X]
59     [AddCommGroup Y] [Module ℝ Y] [AddCommGroup S] [Module ℝ S]
60     (C : X →ₗ[ℝ] Y) (L : X →ₗ[ℝ] X) (h : ℕ)
61     (hc : LinearMap.ker (Delay.observation C L h) ≤
62       LinearMap.ker ((Delay.observation C L h).comp L))
63     (Zm Zp : S →ₗ[ℝ] LinearMap.range (Delay.observation C L h))
64     (coverage : Function.Surjective Zm)
65     (successors : Zp = (Delay.transition C L h hc).comp Zm)
66     (B : LinearMap.range (Delay.observation C L h) →ₗ[ℝ] LinearMap.range (Delay.observation C L h))
67     (fit : B.comp Zm = Zp) : B = Delay.transition C L h hc := by
68   apply LinearMap.ext
69   intro v
70   obtain ⟨x,rfl⟩ := coverage v
71   have he := congrArg (fun F : S →ₗ[ℝ] LinearMap.range (Delay.observation C L h) => F x) fit
72   simpa [successors] using he
73 
74 variable [FiniteDimensional ℝ V]
75 
76 /-- Noisy operator identification is connected to the actual recursively generated trajectory. -/
77 theorem fitted_rollout (A R E' F' : E →L[ℝ] V) (B : V →L[ℝ] V)
78     (hE : ‖E'‖ < rowGain A) (x z : ℕ → V) (M : ℕ → ℝ)
79     (true_step : ∀ t, x (t+1) = B (x t))
80     (pred_step : ∀ t, z (t+1) = ((B.comp A + R + F').comp (pinvL (A+E'))) (z t))
81     (bounded : ∀ t, ‖x t‖ ≤ M t) (T : ℕ) :
82     ‖x T - z T‖ ≤ Stability.errorEnvelope
83       (fun _ => ‖(B.comp A + R + F').comp (pinvL (A+E'))‖)
84       (fun t => ((‖R‖+‖F'‖+‖B‖*‖E'‖)/(rowGain A-‖E'‖))*M t)
85       ‖x 0-z 0‖ T := by
86   let Bh := (B.comp A + R + F').comp (pinvL (A+E'))
87   let q := (‖R‖+‖F'‖+‖B‖*‖E'‖)/(rowGain A-‖E'‖)
88   have hq : 0 ≤ q := by dsimp [q]; positivity
89   have hb : ‖Bh-B‖ ≤ q := noisy_identification_bound A R E' F' B hE
90   apply Stability.recurrence_product_sum (fun t => ‖x t-z t‖)
91     (fun _ => ‖Bh‖) (fun t => q*M t) (fun _ => norm_nonneg _)
92   intro t
93   rw [true_step, pred_step]
94   apply Stability.local_error_step Bh
95   · have hn := (Bh-B).le_opNorm (x t)
96     have hn' : ‖B (x t)-Bh (x t)‖ ≤ ‖Bh-B‖*‖x t‖ := by
97       simpa only [sub_apply, norm_sub_rev] using hn
98     exact hn'.trans (mul_le_mul hb (bounded t) (norm_nonneg _) hq)
99   · simpa only [map_sub] using Bh.le_opNorm (x t-z t)
100 
101 
102 omit [FiniteDimensional ℝ V] in
103 /-- A verified invariant error budget gives an all-time radius. -/
104 theorem rollout_uniform_bound (B Bh : V →L[ℝ] V) (x z : ℕ → V)
105     (delta radius : ℝ)
106     (budget : delta ≤ (1-‖Bh‖)*radius)
107     (initial : ‖x 0-z 0‖ ≤ radius)
108     (true_step : ∀ t, x (t+1) = B (x t)) (pred_step : ∀ t, z (t+1) = Bh (z t))
109     (defect : ∀ t, ‖B (x t)-Bh (x t)‖ ≤ delta) :
110     ∀ t, ‖x t-z t‖ ≤ radius := by
111   intro t
112   induction t with
113   | zero => exact initial
114   | succ t ih =>
115     rw [true_step, pred_step]
116     have he := Stability.local_error_step Bh (x t) (z t) (B (x t)) (defect t)
117       (by simpa only [map_sub] using Bh.le_opNorm (x t-z t))
118     have hm := mul_le_mul_of_nonneg_left ih (norm_nonneg Bh)
119     nlinarith
120 omit [FiniteDimensional ℝ V] in
121 theorem contracting_rollout (B Bh : V →L[ℝ] V) (x z : ℕ → V)
122     (delta : ℝ) (gain : ‖Bh‖ < 1)
123     (true_step : ∀ t, x (t+1) = B (x t)) (pred_step : ∀ t, z (t+1) = Bh (z t))
124     (defect : ∀ t, ‖B (x t)-Bh (x t)‖ ≤ delta) :
125     ∀ t, ‖x t-z t‖ ≤ max ‖x 0-z 0‖ (delta/(1-‖Bh‖)) := by
126   apply rollout_uniform_bound B Bh x z delta
127   · exact (div_le_iff₀ (sub_pos.mpr gain)).mp (le_max_right _ _) |>.trans_eq (mul_comm _ _)
128   · exact le_max_left _ _
129   · exact true_step
130   · exact pred_step
131   · exact defect
132 omit [FiniteDimensional ℝ V] in
133 theorem decoded_rollout_bound {O : Type*} [NormedAddCommGroup O] [NormedSpace ℝ O]
134     (H : V →L[ℝ] O) (x z : V) (bound : ℝ) (hb : ‖x-z‖ ≤ bound) :
135     ‖H x-H z‖ ≤ ‖H‖*bound := by
136   rw [← map_sub]
137   exact (H.le_opNorm (x-z)).trans (mul_le_mul_of_nonneg_left hb (norm_nonneg H))
138 end Komorebi.LSM.Identification

Back to source controls