FiniteTestRows.lean

1 import KomorebiLSM.TestCones
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 
4 /-! Finite half-space representations of test levels. The construction proceeds
5 by adjoining the pullbacks of the current rows under every symbol. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.TestDomains
8 open scoped BigOperators
9 variable {E S : Type*} [AddCommGroup E] [Module ℝ E] [Fintype S]
10 
11 /-- Every finite test level is cut out by a finite set of linear half-spaces. -/
12 theorem finite_test_halfspaces (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (h : ℕ) :
13     ∃ rows : Finset (E →ₗ[ℝ] ℝ), testLevel B l h = {x | ∀ r ∈ rows, 0 ≤ r x} := by
14   classical
15   induction h with
16   | zero => exact ⟨{l},by simp [testLevel_zero]⟩
17   | succ h ih =>
18     obtain ⟨rows,he⟩ := ih
19     let next : Finset (E →ₗ[ℝ] ℝ) := rows ∪ Finset.univ.biUnion
20       (fun s => rows.image (fun r => r.comp (B s)))
21     refine ⟨next, ?_⟩
22     rw [testLevel_succ,he]
23     ext x
24     simp only [Set.mem_inter_iff,Set.mem_ofPred_eq,Set.mem_iInter,Set.mem_preimage]
25     constructor
26     · rintro ⟨hx,hs⟩ r hr
27       rcases Finset.mem_union.mp hr with hr|hr
28       · exact hx r hr
29       · obtain ⟨s,_,hr⟩ := Finset.mem_biUnion.mp hr
30         obtain ⟨q,hq,rfl⟩ := Finset.mem_image.mp hr
31         exact hs s q hq
32     · intro hx
33       constructor
34       · intro r hr
35         exact hx r (Finset.mem_union.mpr (Or.inl hr))
36       · intro s r hr
37         exact hx (r.comp (B s)) (Finset.mem_union.mpr (Or.inr
38           (Finset.mem_biUnion.mpr ⟨s,Finset.mem_univ s,
39             Finset.mem_image.mpr ⟨r,hr,rfl⟩⟩)))
40 
41 /-- Equality of adjacent test levels yields finite constraints for every future. -/
42 theorem finite_stopping_certificate (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
43     (h : ℕ) (he : testLevel B l (h+1) = testLevel B l h) :
44     ∃ rows : Finset (E →ₗ[ℝ] ℝ), allTests B l = {x | ∀ r ∈ rows, 0 ≤ r x} := by
45   rw [← testLevel_stopping B l h he]
46   exact finite_test_halfspaces B l h
47 
48 omit [Fintype S] in
49 /-- The manuscript's dual-span observability condition supplies separation. -/
50 theorem observe_injective_of_row_span (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
51     (hspan : Submodule.span ℝ (Set.range (fun w => l.comp (FiniteInstruments.wordAction B w))) = ⊤) :
52     Function.Injective (observe B l) := by
53   intro x y hxy
54   apply Module.eval_apply_injective ℝ
55   apply LinearMap.ext
56   intro φ
57   have hp : ∀ ψ, ψ ∈ Submodule.span ℝ (Set.range (fun w => l.comp (FiniteInstruments.wordAction B w))) →
58       ψ x = ψ y := by
59     intro ψ hψ
60     induction hψ using Submodule.span_induction with
61     | mem ψ hψ =>
62       obtain ⟨w,rfl⟩ := hψ
63       exact congrFun hxy w
64     | zero => rfl
65     | add ψ χ hψ hχ ihψ ihχ => simp only [LinearMap.add_apply,ihψ,ihχ]
66     | smul c ψ hψ ih => simp only [LinearMap.smul_apply,ih]
67   exact hp φ (by rw [hspan]; trivial)
68 
69 end Komorebi.LSM.TestDomains

Back to source controls