InstrumentCompletion.lean

1 import KomorebiLSM.FiniteInstrument
2 import KomorebiLSM.PredictiveCompletion
3 
4 /-! P26: the bounded invariant completion of the mass row equals the span
5 of all chronological word tests. Minimality is against actual belief readouts. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.FiniteInstruments
8 open scoped BigOperators
9 open Module FiniteBayes
10 universe u v
11 
12 section WordRows
13 variable {X : Type*} [AddCommGroup X] [Module ℝ X] {S : Type*}
14 
15 noncomputable def wordRow (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) (w : List S) :
16     Dual ℝ X := mu.comp (wordAction L w)
17 
18 @[simp] theorem wordRow_nil (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
19     wordRow L mu [] = mu := by simp [wordRow]
20 
21 @[simp] theorem wordRow_cons (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) (s : S) (w : List S) :
22     wordRow L mu (s::w) = (L s).dualMap (wordRow L mu w) := rfl
23 
24 noncomputable def wordSpan (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
25     Submodule ℝ (Dual ℝ X) := Submodule.span ℝ (Set.range (wordRow L mu))
26 
27 theorem wordRow_mem (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) (w : List S) :
28     wordRow L mu w ∈ wordSpan L mu := Submodule.subset_span ⟨w,rfl⟩
29 
30 theorem massRow_mem_wordSpan (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
31     mu ∈ wordSpan L mu := by simpa using wordRow_mem L mu []
32 
33 theorem wordSpan_invariant (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
34     CommonInvariant (fun s => (L s).dualMap) (wordSpan L mu) := by
35   intro s z hz
36   obtain ⟨r,hr,rfl⟩ := Submodule.mem_map.mp hz
37   clear hz
38   induction hr using Submodule.span_induction with
39   | mem r hr =>
40     obtain ⟨w,rfl⟩ := hr
41     exact wordRow_mem L mu (s::w)
42   | zero => simp
43   | add x y hx hy ihx ihy => simpa using (wordSpan L mu).add_mem ihx ihy
44   | smul a x hx ih => simpa using (wordSpan L mu).smul_mem a ih
45 
46 variable [FiniteDimensional ℝ X]
47 
48 /-- The initial row is not assumed to be a fixed point. -/
49 noncomputable def instrumentCompletion (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
50     Submodule ℝ (Dual ℝ X) := predictiveCompletion L (Submodule.span ℝ {mu})
51 
52 theorem massRow_mem_completion (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
53     mu ∈ instrumentCompletion L mu :=
54   (predictiveCompletion_isLeast L _).1.1 (Submodule.subset_span (Set.mem_singleton mu))
55 
56 theorem instrumentCompletion_invariant (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
57     CommonInvariant (fun s => (L s).dualMap) (instrumentCompletion L mu) :=
58   (predictiveCompletion_isLeast L _).1.2
59 
60 theorem wordRow_mem_completion (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) (w : List S) :
61     wordRow L mu w ∈ instrumentCompletion L mu := by
62   induction w with
63   | nil => simpa using massRow_mem_completion L mu
64   | cons s w ih =>
65     exact instrumentCompletion_invariant L mu s (Submodule.mem_map.mpr ⟨_,ih,rfl⟩)
66 
67 /-- The finite iteration recovers exactly the span of all finite tests. -/
68 theorem instrumentCompletion_eq_wordSpan (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X) :
69     instrumentCompletion L mu = wordSpan L mu := by
70   apply le_antisymm
71   · apply invariantCompletion_minimal
72     · apply Submodule.span_le.mpr
73       intro x hx
74       rw [Set.mem_singleton_iff] at hx
75       rw [hx]
76       exact massRow_mem_wordSpan L mu
77     · exact wordSpan_invariant L mu
78   · apply Submodule.span_le.mpr
79     rintro _ ⟨w,rfl⟩
80     exact wordRow_mem_completion L mu w
81 
82 /-- A nonzero mass row starts with dimension one. -/
83 theorem instrumentCompletion_stabilizes (L : S → X →ₗ[ℝ] X) (mu : Dual ℝ X)
84     (hmu : mu ≠ 0) :
85     ∃ n ≤ finrank ℝ X - 1,
86       invariantSequence (fun s => (L s).dualMap) (Submodule.span ℝ {mu}) (n+1) =
87         invariantSequence (fun s => (L s).dualMap) (Submodule.span ℝ {mu}) n := by
88   simpa only [finrank_span_singleton hmu] using
89     predictiveCompletion_stopping_bound L (Submodule.span ℝ {mu})
90 
91 end WordRows
92 
93 section FiniteBeliefs
94 variable {I : Type u} [Fintype I] {S : Type v}
95 variable {E : Type*} [AddCommGroup E] [Module ℝ E]
96 
97 /-- Linear readouts on all priors, not a supplied invariant-row condition. -/
98 def ReadsAllWords (L : S → (I → ℝ) →ₗ[ℝ] (I → ℝ)) (R : (I → ℝ) →ₗ[ℝ] E) : Prop :=
99   ∀ w : List S, ∃ f : E →ₗ[ℝ] ℝ,
100     ∀ p, IsPrior p → f (R p) = mass (wordAction L w p)
101 
102 theorem completion_le_word_reading_summary
103     (L : S → (I → ℝ) →ₗ[ℝ] (I → ℝ)) (R : (I → ℝ) →ₗ[ℝ] E)
104     (h : ReadsAllWords L R) :
105     instrumentCompletion L mass ≤ LinearMap.range R.dualMap := by
106   rw [instrumentCompletion_eq_wordSpan]
107   apply Submodule.span_le.mpr
108   rintro r ⟨w,rfl⟩
109   obtain ⟨f,hf⟩ := h w
110   refine ⟨f, ?_⟩
111   exact linearMap_eq_of_priors (f.comp R) (wordRow L mass w) hf
112 
113 theorem finite_instrument_stopping_bound [Nonempty I]
114     (L : S → (I → ℝ) →ₗ[ℝ] (I → ℝ)) :
115     ∃ n ≤ Fintype.card I - 1,
116       invariantSequence (fun s => (L s).dualMap) (Submodule.span ℝ {mass}) (n+1) =
117         invariantSequence (fun s => (L s).dualMap) (Submodule.span ℝ {mass}) n := by
118   simpa only [Module.finrank_fintype_fun_eq_card] using instrumentCompletion_stabilizes L mass mass_ne_zero
119 
120 end FiniteBeliefs
121 end Komorebi.LSM.FiniteInstruments

Back to source controls