TestCones.lean

1 import KomorebiLSM.FiniteInstrument
2 import Mathlib.Analysis.Convex.Basic
3 
4 /-! P38: finite test hierarchies and the all-test cone. The stopping condition
5 is equality of sets of states, not successful testing of finitely many states. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.TestDomains
8 open scoped BigOperators
9 open FiniteInstruments
10 variable {E S : Type*} [AddCommGroup E] [Module ℝ E]
11 
12 noncomputable def observe (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
13     E →ₗ[ℝ] (List S → ℝ) := LinearMap.pi (fun w => l.comp (wordAction B w))
14 
15 @[simp] theorem observe_apply (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
16     (x : E) (w : List S) : observe B l x w = l (wordAction B w x) := rfl
17 
18 noncomputable def testLevel (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (h : ℕ) : Set E :=
19   {x | ∀ w, w.length ≤ h → 0 ≤ observe B l x w}
20 
21 noncomputable def allTests (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) : Set E :=
22   {x | ∀ w, 0 ≤ observe B l x w}
23 
24 noncomputable def base (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) : Set E :=
25   {x | x ∈ allTests B l ∧ l x = 1}
26 
27 theorem allTests_zero (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
28     (0 : E) ∈ allTests B l := by intro w; simp
29 
30 theorem allTests_add (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
31     {x y : E} (hx : x ∈ allTests B l) (hy : y ∈ allTests B l) :
32     x+y ∈ allTests B l := by
33   intro w
34   simpa only [map_add,Pi.add_apply] using add_nonneg (hx w) (hy w)
35 
36 theorem allTests_smul (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
37     {c : ℝ} (hc : 0 ≤ c) {x : E} (hx : x ∈ allTests B l) :
38     c • x ∈ allTests B l := by
39   intro w
40   simpa only [map_smul,Pi.smul_apply,smul_eq_mul] using mul_nonneg hc (hx w)
41 
42 theorem allTests_convex (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
43     Convex ℝ (allTests B l) := by
44   intro x hx y hy a b ha hb _
45   exact allTests_add B l (allTests_smul B l ha hx) (allTests_smul B l hb hy)
46 
47 theorem base_convex (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
48     Convex ℝ (base B l) := by
49   intro x hx y hy a b ha hb hab
50   refine ⟨allTests_convex B l hx.1 hy.1 ha hb hab, ?_⟩
51   simpa only [map_add,map_smul,smul_eq_mul,hx.2,hy.2,mul_one] using hab
52 
53 theorem allTests_invariant (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
54     (s : S) {x : E} (hx : x ∈ allTests B l) : B s x ∈ allTests B l := by
55   intro w
56   exact hx (s::w)
57 
58 theorem allTests_word (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
59     (w : List S) {x : E} (hx : x ∈ allTests B l) : wordAction B w x ∈ allTests B l := by
60   induction w generalizing x with
61   | nil => exact hx
62   | cons s w ih => exact ih (allTests_invariant B l s hx)
63 
64 theorem allTests_mass_nonneg (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
65     {x : E} (hx : x ∈ allTests B l) : 0 ≤ l x := hx []
66 
67 theorem testLevel_zero (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
68     testLevel B l 0 = {x | 0 ≤ l x} := by
69   ext x
70   constructor
71   · intro hx; exact hx [] (by simp)
72   · intro hx w hw
73     have he : w = [] := List.length_eq_zero_iff.mp (Nat.eq_zero_of_le_zero hw)
74     subst w
75     exact hx
76 
77 /-- One more test step is a preimage refinement by every branch. -/
78 theorem testLevel_succ (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (h : ℕ) :
79     testLevel B l (h+1) = testLevel B l h ∩ ⋂ s, (B s) ⁻¹' testLevel B l h := by
80   ext x
81   constructor
82   · intro hx
83     refine ⟨fun w hw => hx w (hw.trans (Nat.le_succ h)), ?_⟩
84     simp only [Set.mem_iInter,Set.mem_preimage]
85     intro s w hw
86     exact hx (s::w) (by simpa using Nat.succ_le_succ hw)
87   · rintro ⟨hx,hs⟩ w hw
88     cases w with
89     | nil => exact hx [] (Nat.zero_le h)
90     | cons s w =>
91       have hmem := Set.mem_iInter.mp hs s
92       exact hmem w (by simpa using hw)
93 
94 theorem testLevel_antitone (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
95     Antitone (testLevel B l) := by
96   intro h k hhk x hx w hw
97   exact hx w (hw.trans hhk)
98 
99 theorem allTests_eq_inter (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
100     allTests B l = ⋂ h, testLevel B l h := by
101   ext x
102   simp only [Set.mem_iInter]
103   constructor
104   · intro hx h w _; exact hx w
105   · intro hx w; exact hx w.length w le_rfl
106 
107 /-- Any invariant set with nonnegative mass is included in the all-test cone. -/
108 theorem allTests_greatest (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
109     (C : Set E) (hm : ∀ x ∈ C, 0 ≤ l x)
110     (hi : ∀ s x, x ∈ C → B s x ∈ C) : C ⊆ allTests B l := by
111   intro x hx w
112   have hw : wordAction B w x ∈ C := by
113     induction w generalizing x with
114     | nil => exact hx
115     | cons s w ih => exact ih (hi s x hx)
116   exact hm _ hw
117 
118 /-- Exact equality of successive constraints is an all-horizon certificate. -/
119 theorem testLevel_stopping (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (h : ℕ)
120     (he : testLevel B l (h+1) = testLevel B l h) :
121     testLevel B l h = allTests B l := by
122   apply Set.Subset.antisymm
123   · apply allTests_greatest B l (testLevel B l h)
124     · intro x hx; exact hx [] (Nat.zero_le h)
125     · intro s x hx
126       have hx' : x ∈ testLevel B l (h+1) := by rwa [he]
127       rw [testLevel_succ] at hx'
128       exact Set.mem_iInter.mp hx'.2 s
129   · intro x hx w _; exact hx w
130 
131 /-- Observability eliminates the common kernel of all test half-spaces. -/
132 theorem allTests_pointed (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
133     (ho : Function.Injective (observe B l)) {x : E}
134     (hx : x ∈ allTests B l) (hn : -x ∈ allTests B l) : x = 0 := by
135   apply ho
136   funext w
137   have hh := hn w
138   simp only [map_neg,Pi.neg_apply] at hh
139   have hz : observe B l x w = 0 := le_antisymm (neg_nonneg.mp hh) (hx w)
140   simpa using hz
141 
142 /-- Reachable cone vectors span whenever the realization is reachable. -/
143 theorem allTests_spans (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (x₀ : E)
144     (h₀ : x₀ ∈ allTests B l)
145     (hr : Submodule.span ℝ (Set.range (fun w => wordAction B w x₀)) = ⊤) :
146     Submodule.span ℝ (allTests B l) = ⊤ := by
147   apply top_unique
148   rw [← hr]
149   apply Submodule.span_mono
150   rintro _ ⟨w,rfl⟩
151   exact allTests_word B l w h₀
152 
153 section Causal
154 variable {A O : Type*} [Fintype O]
155 variable (B : A × O → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
156 variable (hm : ∀ a x, ∑ o, l (B (a,o) x) = l x)
157 include hm
158 
159 /-- Causal normalization extends to every prefix and every linear state. -/
160 theorem test_sum_next (x : E) (w : List (A × O)) (a : A) :
161     ∑ o, observe B l x (w ++ [(a,o)]) = observe B l x w := by
162   simp only [observe_apply,wordAction_append,wordAction_cons,wordAction_nil,
163     LinearMap.id_comp,LinearMap.comp_apply]
164   exact hm a (wordAction B w x)
165 
166 theorem test_next_le {x : E} (hx : x ∈ allTests B l) (w : List (A × O)) (s : A × O) :
167     observe B l x (w ++ [s]) ≤ observe B l x w := by
168   rw [← test_sum_next B l hm x w s.1]
169   exact Finset.single_le_sum (fun o _ => hx (w ++ [(s.1,o)])) (Finset.mem_univ s.2)
170 
171 theorem test_extension_le {x : E} (hx : x ∈ allTests B l) (w t : List (A × O)) :
172     observe B l x (w ++ t) ≤ observe B l x w := by
173   induction t generalizing w with
174   | nil => simp
175   | cons s t ih =>
176     have h₁ := ih (w ++ [s])
177     have h₂ := test_next_le B l hm hx w s
178     simpa only [List.append_assoc,List.singleton_append] using h₁.trans h₂
179 
180 theorem test_le_mass {x : E} (hx : x ∈ allTests B l) (w : List (A × O)) :
181     observe B l x w ≤ l x := by
182   simpa only [List.nil_append,observe_apply,wordAction_nil,LinearMap.id_apply] using
183     test_extension_le B l hm hx [] w
184 
185 theorem allTests_strict_mass (ho : Function.Injective (observe B l)) {x : E}
186     (hx : x ∈ allTests B l) (hne : x ≠ 0) : 0 < l x := by
187   have hnonneg := allTests_mass_nonneg B l hx
188   by_contra hn
189   have he : l x = 0 := le_antisymm (le_of_not_gt hn) hnonneg
190   apply hne
191   apply ho
192   funext w
193   have hl := test_le_mass B l hm hx w
194   have hz : observe B l x w = 0 := le_antisymm (he ▸ hl) (hx w)
195   simpa using hz
196 
197 theorem base_test_bounds {x : E} (hx : x ∈ base B l) (w : List (A × O)) :
198     0 ≤ observe B l x w ∧ observe B l x w ≤ 1 := by
199   exact ⟨hx.1 w, hx.2 ▸ test_le_mass B l hm hx.1 w⟩
200 
201 end Causal
202 
203 /-- Positive-evidence normalization preserves the full test domain. -/
204 theorem base_posterior (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
205     {x : E} (hx : x ∈ allTests B l) (s : S) (hp : 0 < l (B s x)) :
206     normalize l (B s x) ∈ base B l := by
207   exact ⟨allTests_smul B l (inv_nonneg.mpr hp.le) (allTests_invariant B l s hx),
208     normalize_mass l _ (ne_of_gt hp)⟩
209 
210 end Komorebi.LSM.TestDomains

Back to source controls