MatrixEmbedding.lean

1 import KomorebiLSM.BaseNormTopology
2 import KomorebiLSM.ObservationTree
3 import KomorebiLSM.ConditionalStochasticCompletion
4 import Mathlib.Analysis.Matrix.Order
5 import KomorebiLSM.MatrixOrderUnit
6 
7 /-! Exact finite-dimensional matrix-embedding certificates. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.MatrixEmbedding
10 open scoped BigOperators
11 
12 /-- A symmetric injective matrix realization with an actual positive-definite witness. -/
13 structure Embedding (E D : Type*) [AddCommGroup E] [Module ℝ E] [Fintype D] where
14   J : E →ₗ[ℝ] Matrix D D ℝ
15   symmetric : ∀ z, (J z).IsHermitian
16   injective : Function.Injective J
17   interior : E
18   interior_posDef : (J interior).PosDef
19 
20 namespace Embedding
21 variable {E D : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
22   [Fintype D] (M : Embedding E D)
23 
24 /-- Trace is the mass functional certified by the embedding. -/
25 def mass : E →ₗ[ℝ] ℝ := (Matrix.traceLinearMap D ℝ ℝ).comp M.J
26 
27 /-- The embedded positive-semidefinite cone. -/
28 def cone : Set E := {z | (M.J z).PosSemidef}
29 
30 @[simp] theorem mass_apply (z : E) : M.mass z = Matrix.trace (M.J z) := rfl
31 @[simp] theorem mem_cone (z : E) : z ∈ M.cone ↔ (M.J z).PosSemidef := Iff.rfl
32 
33 theorem cone_zero : (0 : E) ∈ M.cone := by simp [cone, Matrix.PosSemidef.zero]
34 
35 theorem cone_add {x y : E} (hx : x ∈ M.cone) (hy : y ∈ M.cone) :
36     x + y ∈ M.cone := by
37   simpa only [cone, Set.mem_ofPred_eq, map_add] using hx.add hy
38 
39 theorem cone_smul {a : ℝ} (ha : 0 ≤ a) {x : E} (hx : x ∈ M.cone) :
40     a • x ∈ M.cone := by
41   simpa only [cone, Set.mem_ofPred_eq, map_smul] using hx.smul ha
42 
43 theorem cone_closed [FiniteDimensional ℝ E] : IsClosed M.cone :=
44   Matrix.posSemidef_is_closed.preimage M.J.continuous_of_finiteDimensional
45 
46 theorem cone_mass_nonneg {x : E} (hx : x ∈ M.cone) : 0 ≤ M.mass x := by
47   classical
48   exact Finset.sum_nonneg fun i _ => hx.diag_nonneg
49 
50 theorem cone_mass_pos {x : E} (hx : x ∈ M.cone) (hne : x ≠ 0) : 0 < M.mass x := by
51   have hzero : M.mass x ≠ 0 := by
52     intro h
53     have hj : M.J x = M.J 0 := by simpa using hx.trace_eq_zero_iff.mp h
54     exact hne (M.injective hj)
55   exact lt_of_le_of_ne (M.cone_mass_nonneg hx) (Ne.symm hzero)
56 
57 theorem cone_pointed {x : E} (hx : x ∈ M.cone) (hnx : -x ∈ M.cone) : x = 0 := by
58   by_contra hn
59   have hp := M.cone_mass_pos hx hn
60   have hnp := M.cone_mass_nonneg hnx
61   rw [map_neg] at hnp
62   linarith
63 
64 /-- A definite point dominates every symmetric embedded direction. -/
65 theorem exists_positive_decomposition (x : E) :
66     ∃ u ∈ M.cone, ∃ v ∈ M.cone, x = u - v := by
67   classical
68   obtain ⟨a, ha, hp, _⟩ := MatrixOrderUnit.exists_nonnegative_bound
69     (M.J M.interior) (M.J x) M.interior_posDef (M.symmetric x)
70   refine ⟨a • M.interior + x, ?_, a • M.interior, ?_, ?_⟩
71   · simpa only [mem_cone, map_add, map_smul] using hp
72   · exact M.cone_smul ha M.interior_posDef.posSemidef
73   · simp
74 
75 theorem cone_spans : Submodule.span ℝ M.cone = ⊤ := by
76   apply top_unique
77   intro x _
78   obtain ⟨u, hu, v, hv, rfl⟩ := M.exists_positive_decomposition x
79   exact Submodule.sub_mem _ (Submodule.subset_span hu) (Submodule.subset_span hv)
80 
81 /-- All cone axioms follow from injectivity and the actual definite witness. -/
82 noncomputable def coneInstance [FiniteDimensional ℝ E] : BaseNorm.ProbabilityCone E where
83   carrier := M.cone
84   zero_mem := M.cone_zero
85   add_mem := M.cone_add
86   smul_mem := M.cone_smul
87   spans := M.cone_spans
88   mass := M.mass
89   mass_pos := M.cone_mass_pos
90   closed := M.cone_closed
91 
92 @[simp] theorem coneInstance_mem [FiniteDimensional ℝ E] (z : E) :
93     z ∈ M.coneInstance.carrier ↔ (M.J z).PosSemidef := Iff.rfl
94 
95 @[simp] theorem coneInstance_mass [FiniteDimensional ℝ E] : M.coneInstance.mass = M.mass := rfl
96 
97 /-- The normalized trace-one base is compact in the original coordinates. -/
98 theorem base_compact [FiniteDimensional ℝ E] :
99     IsCompact {z | z ∈ M.cone ∧ M.mass z = 1} := M.coneInstance.base_compact
100 
101 /-- A finite weighted congruence, including the empty sum. -/
102 def weightedCongruence {I : Type*} [Fintype I] (w : I → ℝ)
103     (K : I → Matrix D D ℝ) (X : Matrix D D ℝ) : Matrix D D ℝ :=
104   ∑ i, w i • (K i * X * (K i).transpose)
105 
106 theorem weightedCongruence_posSemidef {I : Type*} [Fintype I]
107     (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) (K : I → Matrix D D ℝ)
108     {X : Matrix D D ℝ} (hX : X.PosSemidef) :
109     (weightedCongruence w K X).PosSemidef := by
110   classical
111   apply Matrix.posSemidef_sum
112   intro i _
113   apply Matrix.PosSemidef.smul _ (hw i)
114   simpa only [Matrix.conjTranspose_eq_transpose_of_trivial] using
115     hX.mul_mul_conjTranspose_same (K i)
116 
117 /-- Branch data expose actual nonnegative weights and matrices, rather than assuming positivity. -/
118 structure CongruenceCertificate {S : Type*} (B : S → E →ₗ[ℝ] E) where
119   terms : S → ℕ
120   weight : (s : S) → Fin (terms s) → ℝ
121   weight_nonneg : ∀ s i, 0 ≤ weight s i
122   factor : (s : S) → Fin (terms s) → Matrix D D ℝ
123   identity : ∀ s z, M.J (B s z) = weightedCongruence (weight s) (factor s) (M.J z)
124 
125 variable {S : Type*} {B : S → E →ₗ[ℝ] E}
126 
127 theorem CongruenceCertificate.preserves_cone
128     (cert : M.CongruenceCertificate B) (s : S) {z : E} (hz : z ∈ M.cone) :
129     B s z ∈ M.cone := by
130   change (M.J (B s z)).PosSemidef
131   rw [cert.identity]
132   exact weightedCongruence_posSemidef _ (cert.weight_nonneg s) _ hz
133 
134 theorem CongruenceCertificate.word_cone (cert : M.CongruenceCertificate B)
135     (word : List S) {z : E} (hz : z ∈ M.cone) :
136     FiniteInstruments.wordAction B word z ∈ M.cone := by
137   induction word generalizing z with
138   | nil => exact hz
139   | cons s word ih => exact ih (CongruenceCertificate.preserves_cone M cert s hz)
140 
141 theorem CongruenceCertificate.word_mass_nonneg (cert : M.CongruenceCertificate B)
142     (word : List S) {z : E} (hz : z ∈ M.cone) :
143     0 ≤ M.mass (FiniteInstruments.wordAction B word z) :=
144   M.cone_mass_nonneg (CongruenceCertificate.word_cone M cert word hz)
145 
146 section Probability
147 variable {A O : Type*} [Fintype O] {B : A × O → E →ₗ[ℝ] E}
148 
149 theorem CongruenceCertificate.causal (cert : M.CongruenceCertificate B)
150     (mass_conservation : ∀ a z, ∑ o, M.mass (B (a,o) z) = M.mass z)
151     (z : E) (hz : z ∈ M.cone) (hm : M.mass z = 1) :
152     Behavior.CausalLaw (fun word => M.mass (FiniteInstruments.wordAction B word z)) := by
153   refine ⟨hm, ?_, ?_⟩
154   · intro word
155     exact CongruenceCertificate.word_mass_nonneg M cert word hz
156   · intro history a
157     simpa only [FiniteInstruments.wordAction_append, FiniteInstruments.wordAction_cons,
158       FiniteInstruments.wordAction_nil, LinearMap.id_comp, LinearMap.comp_apply]
159       using mass_conservation a (FiniteInstruments.wordAction B history z)
160 
161 theorem CongruenceCertificate.word_probability (cert : M.CongruenceCertificate B)
162     (mass_conservation : ∀ a z, ∑ o, M.mass (B (a,o) z) = M.mass z)
163     (z : E) (hz : z ∈ M.cone) (hm : M.mass z = 1) (word : List (A × O)) :
164     0 ≤ M.mass (FiniteInstruments.wordAction B word z) ∧
165       M.mass (FiniteInstruments.wordAction B word z) ≤ 1 :=
166   (CongruenceCertificate.causal M cert mass_conservation z hz hm).word_bounds word
167 
168 /-- Exact mass conservation supplies a complete instrument for each intervention. -/
169 theorem CongruenceCertificate.instrument [FiniteDimensional ℝ E]
170     (cert : M.CongruenceCertificate B)
171     (mass_conservation : ∀ a z, ∑ o, M.mass (B (a,o) z) = M.mass z) (a : A) :
172     M.coneInstance.Instrument (fun o => B (a,o)) := by
173   refine ⟨?_, mass_conservation a⟩
174   intro o x hx
175   exact CongruenceCertificate.preserves_cone M cert (a,o) hx
176 
177 /-- Every finite observation tree under a history-dependent intervention is normalized. -/
178 theorem CongruenceCertificate.observation_tree_prior [FiniteDimensional ℝ E]
179     (cert : M.CongruenceCertificate B)
180     (mass_conservation : ∀ a z, ∑ o, M.mass (B (a,o) z) = M.mass z)
181     (policy : List O → A) (n : ℕ) (z : E) (hz : z ∈ M.cone) (hm : M.mass z = 1) :
182     FiniteBayes.IsPrior (ObservationTree.recordLaw M.coneInstance
183       (fun h o => B (policy h,o)) n [] z) := by
184   exact ObservationTree.record_prior M.coneInstance _
185     (fun h => CongruenceCertificate.instrument M cert mass_conservation (policy h))
186     n [] z ⟨hz, hm⟩
187 
188 end Probability
189 
190 section Atlas
191 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
192 
193 /-- Change of coordinates transports the embedding and its definite interior witness together. -/
194 def transport (T : E ≃ₗ[ℝ] F) : Embedding F D where
195   J := M.J.comp T.symm.toLinearMap
196   symmetric z := M.symmetric (T.symm z)
197   injective := M.injective.comp T.symm.injective
198   interior := T M.interior
199   interior_posDef := by simpa using M.interior_posDef
200 
201 @[simp] theorem transport_apply (T : E ≃ₗ[ℝ] F) (z : E) :
202     (M.transport T).J (T z) = M.J z := by simp [transport]
203 
204 @[simp] theorem transport_mass (T : E ≃ₗ[ℝ] F) (z : E) :
205     (M.transport T).mass (T z) = M.mass z := by simp [mass]
206 
207 theorem transport_cone (T : E ≃ₗ[ℝ] F) : (M.transport T).cone = T '' M.cone := by
208   ext z
209   constructor
210   · intro hz
211     exact ⟨T.symm z, hz, T.apply_symm_apply z⟩
212   · rintro ⟨x, hx, rfl⟩
213     simpa only [mem_cone, transport_apply] using hx
214 
215 /-- The same weighted factors certify every conjugated branch in the new atlas. -/
216 def CongruenceCertificate.transport (cert : M.CongruenceCertificate B)
217     (T : E ≃ₗ[ℝ] F) : (M.transport T).CongruenceCertificate
218       (ConditionalStochasticCompletion.atlasOperator T B) where
219   terms := cert.terms
220   weight := cert.weight
221   weight_nonneg := cert.weight_nonneg
222   factor := cert.factor
223   identity s z := by
224     change M.J (T.symm (T (B s (T.symm z)))) = _
225     simpa only [LinearEquiv.symm_apply_apply, Embedding.transport, LinearMap.comp_apply,
226       LinearEquiv.coe_coe] using cert.identity s (T.symm z)
227 
228 theorem transport_word_trace (T : E ≃ₗ[ℝ] F) (word : List S) (z : E) :
229     (M.transport T).mass
230       (FiniteInstruments.wordAction (ConditionalStochasticCompletion.atlasOperator T B)
231         word (T z)) = M.mass (FiniteInstruments.wordAction B word z) := by
232   rw [ConditionalStochasticCompletion.atlas_word, M.transport_mass]
233 
234 end Atlas
235 end Embedding
236 end Komorebi.LSM.MatrixEmbedding

Back to source controls