FiniteInstrument.lean

1 import KomorebiLSM.FiniteBayes
2 import Mathlib.LinearAlgebra.Matrix.ToLin
3 import Mathlib.LinearAlgebra.Dual.Defs
4 
5 /-! Finite nonnegative probability instruments with chronological word semantics.
6 Mass, positivity and the restriction to positive-probability conditioning are explicit. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.FiniteInstruments
9 open scoped BigOperators
10 open FiniteBayes
11 universe u v w
12 variable {I : Type u} {U : Type v} {O : Type w}
13 
14 section Normalization
15 variable {E : Type*} [AddCommGroup E] [Module ℝ E]
16 
17 noncomputable def normalize (l : E →ₗ[ℝ] ℝ) (x : E) : E := (l x)⁻¹ • x
18 
19 theorem normalize_mass (l : E →ₗ[ℝ] ℝ) (x : E) (h : l x ≠ 0) :
20     l (normalize l x) = 1 := by
21   simp [normalize, h]
22 
23 theorem normalize_zero_mass (l : E →ₗ[ℝ] ℝ) (x : E) (h : l x = 0) :
24     normalize l x = 0 := by
25   simp [normalize, h]
26 
27 theorem recover_from_normalize (l : E →ₗ[ℝ] ℝ) (x : E) (h : l x ≠ 0) :
28     l x • normalize l x = x := by
29   simp [normalize, smul_smul, h]
30 
31 end Normalization
32 
33 section FiniteMass
34 variable [Fintype I]
35 
36 noncomputable def mass : (I → ℝ) →ₗ[ℝ] ℝ := ∑ i, LinearMap.proj i
37 
38 @[simp] theorem mass_apply (p : I → ℝ) : mass p = ∑ i, p i := by
39   simp [mass, LinearMap.sum_apply]
40 
41 theorem mass_prior (p : I → ℝ) (hp : IsPrior p) : mass p = 1 := by
42   simpa only [mass_apply] using hp.2
43 
44 theorem mass_nonneg (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) : 0 ≤ mass p := by
45   rw [mass_apply]
46   exact Finset.sum_nonneg (fun i _ => hp i)
47 
48 theorem normalized_prior (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (hm : 0 < mass p) :
49     IsPrior (normalize mass p) := by
50   refine ⟨fun i => mul_nonneg (inv_nonneg.mpr hm.le) (hp i), ?_⟩
51   simpa only [mass_apply] using normalize_mass mass p (ne_of_gt hm)
52 
53 theorem vector_eq_sum_pointMass [DecidableEq I] (p : I → ℝ) :
54     p = ∑ i, p i • pointMass i := by
55   funext j
56   simp [pointMass, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
57 
58 theorem point_prior [DecidableEq I] (i : I) : IsPrior (pointMass i) := by
59   constructor
60   · intro j; simp only [pointMass]; positivity
61   · simp [pointMass]
62 
63 theorem mass_pointMass [DecidableEq I] (i : I) : mass (pointMass i) = 1 :=
64   mass_prior _ (point_prior i)
65 
66 theorem mass_ne_zero [Nonempty I] : (mass : (I → ℝ) →ₗ[ℝ] ℝ) ≠ 0 := by
67   classical
68   intro h
69   let i : I := Classical.choice inferInstance
70   have he := mass_pointMass i
71   rw [h] at he
72   norm_num at he
73 
74 /-- Equality on all beliefs determines a linear map on the entire vector space. -/
75 theorem linearMap_eq_of_priors {E : Type*} [AddCommGroup E] [Module ℝ E]
76     (F G : (I → ℝ) →ₗ[ℝ] E)
77     (h : ∀ p, IsPrior p → F p = G p) : F = G := by
78   classical
79   apply LinearMap.ext
80   intro p
81   rw [vector_eq_sum_pointMass p, map_sum, map_sum]
82   apply Finset.sum_congr rfl
83   intro i _
84   simp only [map_smul, h _ (point_prior i)]
85 
86 end FiniteMass
87 
88 section Words
89 variable {X : Type*} [AddCommGroup X] [Module ℝ X] {S : Type*}
90 
91 /-- Symbols are listed in time order. The head acts first. -/
92 def wordAction (L : S → X →ₗ[ℝ] X) : List S → X →ₗ[ℝ] X
93   | [] => LinearMap.id
94   | s :: w => (wordAction L w).comp (L s)
95 
96 @[simp] theorem wordAction_nil (L : S → X →ₗ[ℝ] X) : wordAction L [] = LinearMap.id := rfl
97 
98 @[simp] theorem wordAction_cons (L : S → X →ₗ[ℝ] X) (s : S) (w : List S) :
99     wordAction L (s::w) = (wordAction L w).comp (L s) := rfl
100 
101 theorem wordAction_append (L : S → X →ₗ[ℝ] X) (v w : List S) :
102     wordAction L (v++w) = (wordAction L w).comp (wordAction L v) := by
103   induction v with
104   | nil => simp
105   | cons s v ih => simp [ih, LinearMap.comp_assoc]
106 
107 theorem word_intertwining {E : Type*} [AddCommGroup E] [Module ℝ E]
108     (L : S → X →ₗ[ℝ] X) (B : S → E →ₗ[ℝ] E) (R : X →ₗ[ℝ] E)
109     (h : ∀ s, (B s).comp R = R.comp (L s)) (w : List S) :
110     (wordAction B w).comp R = R.comp (wordAction L w) := by
111   induction w with
112   | nil => simp
113   | cons s w ih =>
114     rw [wordAction_cons, wordAction_cons, LinearMap.comp_assoc, h s,
115       ← LinearMap.comp_assoc, ih, LinearMap.comp_assoc]
116 
117 end Words
118 
119 /-- The branch entry (j,i) is joint next-state/observation probability. -/
120 structure Instrument (I : Type u) (U : Type v) (O : Type w) [Fintype I] [Fintype O] where
121   matrix : U → O → Matrix I I ℝ
122   nonneg : ∀ a o j i, 0 ≤ matrix a o j i
123   mass_one : ∀ a i, ∑ o, ∑ j, matrix a o j i = 1
124 
125 namespace Instrument
126 variable [Fintype I] [Fintype O]
127 variable (T : Instrument I U O)
128 
129 noncomputable def branch (s : U × O) : (I → ℝ) →ₗ[ℝ] (I → ℝ) :=
130   (T.matrix s.1 s.2).mulVecLin
131 
132 @[simp] theorem branch_apply (s : U × O) (p : I → ℝ) (j : I) :
133     T.branch s p j = ∑ i, T.matrix s.1 s.2 j i * p i := rfl
134 
135 theorem branch_nonneg (s : U × O) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
136     ∀ j, 0 ≤ T.branch s p j := by
137   intro j
138   exact Finset.sum_nonneg (fun i _ => mul_nonneg (T.nonneg _ _ _ _) (hp i))
139 
140 theorem instrument_mass (a : U) (p : I → ℝ) :
141     ∑ o, mass (T.branch (a,o) p) = mass p := by
142   simp only [mass_apply, branch_apply]
143   conv_lhs => arg 2; ext o; rw [Finset.sum_comm]
144   rw [Finset.sum_comm]
145   apply Finset.sum_congr rfl
146   intro i _
147   simp only [← Finset.sum_mul, T.mass_one, one_mul]
148 
149 theorem instrument_mass_linear (a : U) :
150     ∑ o, mass.comp (T.branch (a,o)) = mass := by
151   ext p
152   simpa only [LinearMap.sum_apply, LinearMap.comp_apply] using T.instrument_mass a p
153 
154 theorem branch_mass_nonneg (s : U × O) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
155     0 ≤ mass (T.branch s p) := mass_nonneg _ (T.branch_nonneg s p hp)
156 
157 theorem branch_mass_le (a : U) (o : O) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
158     mass (T.branch (a,o) p) ≤ mass p := by
159   rw [← T.instrument_mass a p]
160   exact Finset.single_le_sum (fun o _ => T.branch_mass_nonneg (a,o) p hp) (Finset.mem_univ o)
161 
162 theorem likelihood_prior (a : U) (p : I → ℝ) (hp : IsPrior p) :
163     IsPrior (fun o => mass (T.branch (a,o) p)) := by
164   exact ⟨fun o => T.branch_mass_nonneg (a,o) p hp.1,
165     (T.instrument_mass a p).trans (mass_prior p hp)⟩
166 
167 theorem branch_posterior_prior (s : U × O) (p : I → ℝ) (hp : IsPrior p)
168     (h : 0 < mass (T.branch s p)) : IsPrior (normalize mass (T.branch s p)) :=
169   normalized_prior _ (T.branch_nonneg s p hp.1) h
170 
171 theorem word_nonneg (w : List (U × O)) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
172     ∀ i, 0 ≤ wordAction T.branch w p i := by
173   induction w generalizing p with
174   | nil => exact hp
175   | cons s w ih => exact ih _ (T.branch_nonneg s p hp)
176 
177 theorem word_mass_le (w : List (U × O)) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
178     mass (wordAction T.branch w p) ≤ mass p := by
179   induction w generalizing p with
180   | nil => exact le_rfl
181   | cons s w ih =>
182     exact (ih _ (T.branch_nonneg s p hp)).trans (T.branch_mass_le s.1 s.2 p hp)
183 
184 theorem word_probability (w : List (U × O)) (p : I → ℝ) (hp : IsPrior p) :
185     0 ≤ mass (wordAction T.branch w p) ∧ mass (wordAction T.branch w p) ≤ 1 := by
186   exact ⟨mass_nonneg _ (T.word_nonneg w p hp.1),
187     (T.word_mass_le w p hp.1).trans_eq (mass_prior p hp)⟩
188 
189 /-- Total weight of the observation tree for a fixed action list. -/
190 noncomputable def observationTreeMass : List U → (I → ℝ) → ℝ
191   | [], p => mass p
192   | a::as, p => ∑ o, observationTreeMass as (T.branch (a,o) p)
193 
194 theorem observationTreeMass_eq (as : List U) (p : I → ℝ) :
195     T.observationTreeMass as p = mass p := by
196   induction as generalizing p with
197   | nil => rfl
198   | cons a as ih =>
199     change (∑ o, T.observationTreeMass as (T.branch (a,o) p)) = mass p
200     simp only [ih, T.instrument_mass]
201 
202 end Instrument
203 end Komorebi.LSM.FiniteInstruments

Back to source controls