Block8Examples.lean

1 import KomorebiLSM.MemoryApproximation
2 import KomorebiLSM.StrongRefinement
3 import Mathlib.Tactic.NormNum
4 
5 /-! Exact examples for the distinction between local residuals, propagated
6 error, finite memory and switching. -/
7 set_option autoImplicit false
8 open scoped BigOperators
9 namespace Komorebi.LSM.Block8Examples
10 open Komorebi.LSM.Stability
11 
12 noncomputable def scale (r : ℝ) : ℝ →L[ℝ] ℝ := r • ContinuousLinearMap.id ℝ ℝ
13 
14 @[simp] theorem scale_apply (r x : ℝ) : scale r x = r*x := rfl
15 
16 theorem scale_norm (r : ℝ) : ‖scale r‖=|r| := by simp only [scale,norm_smul,ContinuousLinearMap.norm_id,Real.norm_eq_abs,mul_one]
17 
18 /-- An actual predicted trajectory with local error one and gain two. -/
19 def expandingPrediction (t : ℕ) : ℝ := 2^t-1
20 
21 theorem expandingPrediction_step (t : ℕ) :
22     expandingPrediction (t+1)=2*expandingPrediction t+1 := by
23   simp only [expandingPrediction,pow_succ]
24   ring
25 
26 theorem expanding_lipschitz : LipschitzWith (2 : NNReal) (fun x : ℝ => 2*x+1) := by
27   apply LipschitzWith.of_dist_le_mul
28   intro x y
29   simp only [dist_eq_norm,Real.norm_eq_abs,NNReal.coe_ofNat]
30   rw [show (2*x+1)-(2*y+1)=2*(x-y) by ring,abs_mul]
31   norm_num
32 
33 theorem expanding_prediction_general_bound (T : ℕ) :
34     ‖(0 : ℝ)-expandingPrediction T‖ ≤ errorEnvelope (fun _ => 2) (fun _ => 1) 0 T := by
35   have h := compositional_defect_propagation
36     (X:=ℝ) (Z:=fun _ => ℝ) (fun _ x => x) (fun _ _ => 0)
37     (fun _ x => 2*x+1) (fun _ => 0) expandingPrediction
38     (fun _ => Set.univ) (fun _ => (2 : NNReal)) (fun _ => 1)
39     (fun _ => rfl) expandingPrediction_step
40     (fun _ => Set.mem_univ _) (fun _ => Set.mem_univ _)
41     (fun _ => expanding_lipschitz.lipschitzOnWith) (fun _ => by norm_num) T
42   simpa only [expandingPrediction,Nat.cast_zero,pow_zero,sub_self,norm_zero,NNReal.coe_ofNat] using h
43 
44 theorem expanding_envelope_exact (T : ℕ) :
45     errorEnvelope (fun _ => 2) (fun _ => 1) 0 T=2^T-1 := by
46   induction T with
47   | zero => simp
48   | succ T ih => rw [errorEnvelope_succ,ih,pow_succ]; ring
49 
50 theorem local_error_not_whole_trajectory_error :
51     ‖(0 : ℝ)-expandingPrediction 3‖=7 := by norm_num [expandingPrediction]
52 
53 /-- A stable length-one memory prediction, stored as current/previous values. -/
54 noncomputable def memoryPair : ℕ → ℝ×ℝ
55   | 0 => (0,0)
56   | t+1 => ((memoryPair t).1/2+(memoryPair t).2/4+1/8,(memoryPair t).1)
57 
58 noncomputable def memoryPrediction (s : ℤ) : ℝ :=
59   if 0 ≤ s then (memoryPair s.toNat).1 else 0
60 
61 @[simp] theorem memoryPrediction_nat (t : ℕ) : memoryPrediction (t:ℤ)=(memoryPair t).1 := by
62   simp [memoryPrediction]
63 
64 theorem memoryPrediction_previous (t : ℕ) :
65     memoryPrediction ((t:ℤ)-1)=(memoryPair t).2 := by
66   cases t with
67   | zero => norm_num [memoryPrediction,memoryPair]
68   | succ t =>
69     have h : ((t+1:ℕ):ℤ)-1=(t:ℤ) := by omega
70     rw [h,memoryPrediction_nat]
71     rfl
72 
73 theorem memoryPrediction_initial (s : ℤ) (hs : s ≤ 0) : memoryPrediction s=0 := by
74   rcases eq_or_lt_of_le hs with h|h
75   · subst s; norm_num [memoryPrediction,memoryPair]
76   · simp [memoryPrediction,not_le.mpr h]
77 
78 theorem memoryPrediction_step (t : ℕ) :
79     memoryPrediction ((t:ℤ)+1)=
80       finiteMemory (scale (1/2)) (fun _ => scale (1/4)) 1 memoryPrediction t+1/8 := by
81   rw [show (t:ℤ)+1=((t+1:ℕ):ℤ) by omega,memoryPrediction_nat]
82   rw [finiteMemory,Finset.sum_range_one]
83   simp only [Nat.cast_zero,sub_zero]
84   change (memoryPair (t+1)).1 =
85     (1/2)*memoryPrediction (t:ℤ)+(1/4)*memoryPrediction ((t:ℤ)-1)+1/8
86   rw [memoryPrediction_nat,memoryPrediction_previous]
87   simp only [memoryPair]
88   ring
89 
90 theorem stable_memory_gain : memoryGain (scale (1/2)) (fun _ => scale (1/4)) 1=3/4 := by
91   norm_num [memoryGain,scale_norm]
92 
93 /-- This invokes the general theorem on a predicted trajectory's own history. -/
94 theorem recursive_memory_uniform_bound :
95     sSup (Set.range (fun t : ℕ => ‖(0 : ℝ)-memoryPrediction t‖)) ≤ 1/2 := by
96   have h := finite_memory_uniform_prediction_bound
97     (scale (1/2)) (fun _ => scale (1/4)) 1 (fun _ => (0:ℝ)) memoryPrediction (fun _ => 1/8)
98     (D:=1/8) (E0:=0) (by rw [stable_memory_gain]; norm_num) (by norm_num)
99     (fun s _ hs => by rw [memoryPrediction_initial s hs]; norm_num)
100     memoryPrediction_step (fun _ => by norm_num [finiteMemory])
101   rw [stable_memory_gain] at h
102   norm_num at h ⊢
103   exact h
104 
105 theorem memoryPrediction_first_three :
106     memoryPrediction 1=1/8 ∧ memoryPrediction 2=3/16 ∧ memoryPrediction 3=1/4 := by
107   have h1 := memoryPrediction_nat 1
108   have h2 := memoryPrediction_nat 2
109   have h3 := memoryPrediction_nat 3
110   norm_num [memoryPair] at h1 h2 h3
111   exact ⟨h1,h2,h3⟩
112 
113 /-- The zero-memory-length case still has a well-defined transition. -/
114 theorem zero_memory_length (A : ℝ →L[ℝ] ℝ) (K : ℕ → ℝ →L[ℝ] ℝ) (z : ℤ → ℝ) (t : ℤ) :
115     finiteMemory A K 0 z t=A (z t) := by simp [finiteMemory]
116 
117 /-- Gain one and a persistent local residual can have arbitrarily large error. -/
118 theorem gain_one_drift (t : ℕ) :
119     ((t+1:ℕ):ℝ)=finiteMemory (scale 1) (fun _ => scale 0) 0 (fun s : ℤ => (s:ℝ)) t+1 := by
120   simp [finiteMemory]
121 
122 theorem gain_one_unbounded : ∀ E : ℝ, ∃ t : ℕ, E < ‖(0 : ℝ)-(t:ℝ)‖ := by
123   intro E
124   obtain ⟨t, ht⟩ := exists_nat_gt E
125   exact ⟨t,by simpa using ht⟩
126 
127 /-- Each map squares to zero; their alternating product amplifies a state. -/
128 def switchA : (ℝ×ℝ) →ₗ[ℝ] (ℝ×ℝ) where
129   toFun x := (2*x.2,0)
130   map_add' := by intro x y; ext <;> simp [mul_add]
131   map_smul' := by intro r x; ext <;> simp [mul_left_comm]
132 
133 def switchB : (ℝ×ℝ) →ₗ[ℝ] (ℝ×ℝ) where
134   toFun x := (0,2*x.1)
135   map_add' := by intro x y; ext <;> simp [mul_add]
136   map_smul' := by intro r x; ext <;> simp [mul_left_comm]
137 
138 theorem individually_nilpotent : switchA.comp switchA=0 ∧ switchB.comp switchB=0 := by
139   constructor
140   · apply LinearMap.ext
141     intro x
142     simp [switchA]
143   · apply LinearMap.ext
144     intro x
145     simp [switchB]
146 
147 theorem alternating_amplification (n : ℕ) :
148     ((switchB.comp switchA)^n) (0,1)=(0,4^n) := by
149   induction n with
150   | zero => simp
151   | succ n ih =>
152     rw [pow_succ',Module.End.mul_apply,ih]
153     simp [switchA,switchB,pow_succ']
154     ring
155 
156 theorem alternating_three_pairs : ‖((switchB.comp switchA)^3) (0,1)‖=64 := by
157   rw [alternating_amplification]
158   norm_num
159 
160 end Komorebi.LSM.Block8Examples

Back to source controls