CertificateLearning.lean

1 import KomorebiLSM.BaseNormModels
2 import KomorebiLSM.PolicyComparison
3 import KomorebiLSM.Conditioning
4 import KomorebiLSM.ConditionalStochasticCompletion
5 import Mathlib.MeasureTheory.Measure.Real
6 
7 /-! P49: observable models with finite, checked probability-domain witnesses.
8 Statistical coverage is an explicit event, while stochastic validity follows
9 from the actual nonnegative coefficient matrices and normalized initial lift. -/
10 set_option autoImplicit false
11 namespace Komorebi.LSM.CertificateLearning
12 open scoped BigOperators
13 open FiniteInstruments FiniteBayes PositiveLift BaseNorm ObservationTree
14 
15 variable {E A O J : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
16 variable [FiniteDimensional ℝ E] [Fintype A] [Fintype O] [Fintype J] [DecidableEq J]
17 
18 /-- A stationary finite-dimensional model is its symbol family and initial state. -/
19 abbrev Model (E A O : Type*) [AddCommGroup E] [Module ℝ E] :=
20   (A × O → E →ₗ[ℝ] E) × E
21 
22 /-- A finite witness consists of literal nonnegative matrices and a prior.
23 It assumes no probability-law conclusion. -/
24 structure Witness (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (m : Model E A O) where
25   matrix : A × O → Matrix J J ℝ
26   coefficients : J → ℝ
27   entries_nonnegative : ∀ s i j, 0 ≤ matrix s i j
28   prior : IsPrior coefficients
29   intertwines : ∀ s, (m.1 s).comp V=V.comp (matrix s).mulVecLin
30   mass_law : ∀ a x, ∑ o, l (m.1 (a,o) x)=l x
31   initial : m.2=V coefficients
32 
33 variable (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
34 variable (hn : l.comp V=FiniteInstruments.mass) (hs : Function.Surjective V)
35 
36 omit [FiniteDimensional ℝ E] [Fintype A] in
37 /-- Checked lift equalities imply invariance, rather than assuming validity. -/
38 theorem witness_valid_family {m : Model E A O} (w : Witness V l m) :
39     RobustDomains.ValidFamily (hull V) l m.1 := by
40   refine ⟨?_,w.mass_law⟩
41   intro s
42   exact (positive_lift_iff V (m.1 s)).mpr ⟨w.matrix s,w.entries_nonnegative s,w.intertwines s⟩
43 
44 omit [FiniteDimensional ℝ E] [Fintype A] [DecidableEq J] in
45 include hn in
46 theorem witness_initial {m : Model E A O} (w : Witness V l m) :
47     m.2∈normalizedHull V l := by
48   rw [w.initial]
49   refine ⟨⟨w.coefficients,w.prior.1,rfl⟩,?_⟩
50   simpa only [normalized_mass V l hn] using w.prior.2
51 
52 omit [FiniteDimensional ℝ E] [Fintype A] in
53 include hn in
54 /-- The matrix/prior witness is equivalent to finite-cone validity and initial
55 coverage; the reverse direction constructs its nonnegative columns. -/
56 theorem witness_exists_iff (m : Model E A O) :
57     Nonempty (Witness V l m) ↔
58       RobustDomains.ValidFamily (hull V) l m.1 ∧ m.2∈normalizedHull V l := by
59   classical
60   constructor
61   · rintro ⟨w⟩
62     exact ⟨witness_valid_family V l w,witness_initial V l hn w⟩
63   · rintro ⟨hv,hi⟩
64     have hmat := fun s => (positive_lift_iff V (m.1 s)).mp (hv.1 s)
65     choose M hp he using hmat
66     rw [normalizedHull_eq_prior_image V l hn] at hi
67     obtain ⟨a,ha,heq⟩ := hi
68     exact ⟨⟨M,a,hp,ha,he,hv.2,heq.symm⟩⟩
69 
70 omit [FiniteDimensional ℝ E] [Fintype A] in
71 include hn in
72 /-- Finite robust vertex checks cover every operator family in the actual
73 uncertainty hull; initial-state coverage remains a separate required check. -/
74 theorem robust_vertex_witness {I : Type*}
75     (families : I → A × O → E →ₗ[ℝ] E) (M : I → A × O → Matrix J J ℝ)
76     (hp : ∀ i s j k, 0≤M i s j k)
77     (he : ∀ i s, (families i s).comp V=V.comp (M i s).mulVecLin)
78     (hm : ∀ i a x, ∑ o, l (families i (a,o) x)=l x)
79     (U : Set (Model E A O))
80     (hU : ∀ m∈U, m.1∈convexHull ℝ (Set.range families) ∧ m.2∈normalizedHull V l) :
81     ∀ m∈U, Nonempty (Witness V l m) := by
82   intro m hmem
83   obtain ⟨hB,hinit⟩ := hU m hmem
84   exact (witness_exists_iff V l hn m).mpr
85     ⟨RobustDomains.robust_positive_lift V l families M hp he hm m.1 hB,hinit⟩
86 
87 omit [FiniteDimensional ℝ E] [Fintype A] in
88 include hn in
89 /-- Every future experiment probability is an actual probability of the
90 constructed finite nonnegative instrument, for all word lengths. -/
91 theorem certified_all_words {m : Model E A O} (w : Witness V l m) :
92     (∀ word, 0≤l (wordAction m.1 word m.2) ∧ l (wordAction m.1 word m.2)≤1) := by
93   intro word
94   rw [w.initial]
95   exact (finite_positive_lift_certificate m.1 V l hn w.mass_law w.matrix
96     w.intertwines w.entries_nonnegative w.coefficients w.prior).2.2 word
97 
98 omit [FiniteDimensional ℝ E] [Fintype A] [DecidableEq J] in
99 /-- In a reachable realization an invariant lift containing the initial state
100 already spans the entire observable space. -/
101 theorem witness_surjective_of_reachable {f : List (A × O) → ℝ}
102     (r : Behavior.Realization f E) (hr : r.IsReachable)
103     (w : Witness V l (r.operator,r.initial)) : Function.Surjective V := by
104   apply LinearMap.range_eq_top.mp
105   apply top_unique
106   rw [← hr]
107   apply Submodule.span_le.mpr
108   rintro _ ⟨word,rfl⟩
109   refine ⟨wordAction (fun s => (w.matrix s).mulVecLin) word w.coefficients,?_⟩
110   change V (wordAction (fun s => (w.matrix s).mulVecLin) word w.coefficients)=
111     wordAction r.operator word r.initial
112   have hi : r.initial=V w.coefficients := w.initial
113   exact (PositiveLift.lifted_word r.operator V w.matrix w.intertwines word w.coefficients).symm.trans
114     (congrArg (wordAction r.operator word) hi.symm)
115 
116 omit [Fintype A] in
117 /-- The actual finite witness constructs a full instrument on the common base norm cone. -/
118 theorem certified_instrument {m : Model E A O} (w : Witness V l m) (a : A) :
119     (finiteCone V l hn hs).Instrument (fun o => m.1 (a,o)) := by
120   have hv := witness_valid_family V l w
121   exact ⟨fun o x hx => hv.1 (a,o) x hx,hv.2 a⟩
122 
123 omit [Fintype A] in
124 theorem certified_initial {m : Model E A O} (w : Witness V l m) :
125     m.2∈(finiteCone V l hn hs).base := witness_initial V l hn w
126 
127 /-- Full joint action/observation record law under one common history policy. -/
128 noncomputable def modelLaw (π : List (A × O) → A → ℝ) (n : ℕ)
129     (m : Model E A O) : Record (A × O) n → ℝ :=
130   recordLaw (finiteCone V l hn hs) (policyBranches π (fun _ => m.1)) n [] m.2
131 
132 noncomputable def observedLaw (π : List (A × O) → A → ℝ) (n : ℕ)
133     (m : Model E A O) : Record O n → ℝ :=
134   observationLaw (finiteCone V l hn hs) π (fun _ => m.1) n m.2
135 
136 noncomputable def budget (e₀ : ℝ) (ε : ℕ → ℝ) (n : ℕ) : ℝ :=
137   min 1 ((e₀+∑ t∈Finset.range n, ε t)/2)
138 
139 theorem modelLaw_prior {m : Model E A O} (w : Witness V l m)
140     (π : List (A × O) → A → ℝ) (hπ : ∀ h,IsPrior (π h)) (n : ℕ) :
141     IsPrior (modelLaw V l hn hs π n m) := by
142   apply record_prior (finiteCone V l hn hs)
143     (policyBranches π (fun _ => m.1))
144     (policy_instrument (finiteCone V l hn hs) π hπ (fun _ => m.1)
145       (fun _ a => certified_instrument V l hn hs w a)) n [] m.2
146   exact certified_initial V l hn hs w
147 
148 theorem observedLaw_prior {m : Model E A O} (w : Witness V l m)
149     (π : List (A × O) → A → ℝ) (hπ : ∀ h,IsPrior (π h)) (n : ℕ) :
150     IsPrior (observedLaw V l hn hs π n m) := by
151   classical
152   exact aggregate_prior (recordMap Prod.snd) _ (modelLaw_prior V l hn hs w π hπ n)
153 
154 /-- P49's common-policy bound uses the actual finite-cone infimum and actual
155 record laws. Initial and one-step errors remain explicit numerical budgets. -/
156 theorem certified_policy_bounds {truth fitted : Model E A O}
157     (wt : Witness V l truth) (wf : Witness V l fitted) (ε : ℕ → ℝ) (e₀ : ℝ)
158     (herr : ∀ t a z, z∈(finiteCone V l hn hs).base →
159       (finiteCone V l hn hs).discrepancy (fun o => truth.1 (a,o))
160         (fun o => fitted.1 (a,o)) z≤ε t)
161     (hinit : (finiteCone V l hn hs).value (truth.2-fitted.2)≤e₀)
162     (π : List (A × O) → A → ℝ) (hπ : ∀ h,IsPrior (π h)) (n : ℕ) :
163     FiniteTV.distance (modelLaw V l hn hs π n truth) (modelLaw V l hn hs π n fitted)≤budget e₀ ε n ∧
164     FiniteTV.distance (observedLaw V l hn hs π n truth) (observedLaw V l hn hs π n fitted)≤budget e₀ ε n := by
165   have hb := shared_randomized_policy_tv_bound (finiteCone V l hn hs) π hπ
166     (fun _ => truth.1) (fun _ => fitted.1)
167     (fun _ a => certified_instrument V l hn hs wt a)
168     (fun _ a => certified_instrument V l hn hs wf a) ε
169     (fun h a z hz => herr h.length a z hz) n truth.2 fitted.2
170     (certified_initial V l hn hs wt) (certified_initial V l hn hs wf)
171   have ho := shared_policy_observation_tv_bound (finiteCone V l hn hs) π hπ
172     (fun _ => truth.1) (fun _ => fitted.1)
173     (fun _ a => certified_instrument V l hn hs wt a)
174     (fun _ a => certified_instrument V l hn hs wf a) ε
175     (fun h a z hz => herr h.length a z hz) n truth.2 fitted.2
176     (certified_initial V l hn hs wt) (certified_initial V l hn hs wf)
177   have hbudget : min 1 ((finiteCone V l hn hs).value (truth.2-fitted.2)/2+
178       (∑ t∈Finset.range n, ε t)/2)≤budget e₀ ε n := by
179     apply min_le_min le_rfl
180     linarith
181   exact ⟨hb.trans hbudget,ho.trans hbudget⟩
182 
183 /-- Conditioning applies to those same record laws, with the positive-event
184 premises from P44 rather than an unconditional posterior stability claim. -/
185 theorem certified_conditioning {truth fitted : Model E A O}
186     (wt : Witness V l truth) (wf : Witness V l fitted) (ε : ℕ → ℝ) (e₀ : ℝ)
187     (herr : ∀ t a z, z∈(finiteCone V l hn hs).base →
188       (finiteCone V l hn hs).discrepancy (fun o => truth.1 (a,o))
189         (fun o => fitted.1 (a,o)) z≤ε t)
190     (hinit : (finiteCone V l hn hs).value (truth.2-fitted.2)≤e₀)
191     (π : List (A × O) → A → ℝ) (hπ : ∀ h,IsPrior (π h)) (n : ℕ)
192     [DecidableEq (Record (A × O) n)] (H : Finset (Record (A × O) n))
193     (ht : 0<FiniteTV.eventMass (modelLaw V l hn hs π n truth) H)
194     (hf : 0<FiniteTV.eventMass (modelLaw V l hn hs π n fitted) H) :
195     FiniteTV.distance (FiniteTV.conditional (modelLaw V l hn hs π n truth) H)
196       (FiniteTV.conditional (modelLaw V l hn hs π n fitted) H)≤
197         min 1 (budget e₀ ε n/FiniteTV.eventMass (modelLaw V l hn hs π n truth) H) :=
198   FiniteTV.conditioning_tv_bound _ _ (modelLaw_prior V l hn hs wt π hπ n)
199     (modelLaw_prior V l hn hs wf π hπ n) H (budget e₀ ε n)
200     (certified_policy_bounds V l hn hs wt wf ε e₀ herr hinit π hπ n).1 ht hf
201 
202 /-- P44 also conditions the actual observation-only record laws, with both
203 positive-event denominator hypotheses retained. -/
204 theorem certified_observation_conditioning {truth fitted : Model E A O}
205     (wt : Witness V l truth) (wf : Witness V l fitted) (ε : ℕ → ℝ) (e₀ : ℝ)
206     (herr : ∀ t a z,z∈(finiteCone V l hn hs).base →
207       (finiteCone V l hn hs).discrepancy (fun o => truth.1 (a,o))
208         (fun o => fitted.1 (a,o)) z≤ε t)
209     (hinit : (finiteCone V l hn hs).value (truth.2-fitted.2)≤e₀)
210     (π : List (A × O) → A → ℝ) (hπ : ∀ h,IsPrior (π h)) (n : ℕ)
211     [DecidableEq (Record O n)] (H : Finset (Record O n))
212     (ht : 0<FiniteTV.eventMass (observedLaw V l hn hs π n truth) H)
213     (hf : 0<FiniteTV.eventMass (observedLaw V l hn hs π n fitted) H) :
214     FiniteTV.distance (FiniteTV.conditional (observedLaw V l hn hs π n truth) H)
215       (FiniteTV.conditional (observedLaw V l hn hs π n fitted) H)≤
216         min 1 (budget e₀ ε n/FiniteTV.eventMass (observedLaw V l hn hs π n truth) H) :=
217   FiniteTV.conditioning_tv_bound _ _ (observedLaw_prior V l hn hs wt π hπ n)
218     (observedLaw_prior V l hn hs wf π hπ n) H (budget e₀ ε n)
219     (certified_policy_bounds V l hn hs wt wf ε e₀ herr hinit π hπ n).2 ht hf
220 
221 section Confidence
222 open MeasureTheory
223 variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
224 
225 omit [IsProbabilityMeasure μ] in
226 /-- P49's confidence event is supplied by the justified observation protocol.
227 On it actual robust coefficient certificates make the true and fitted models
228 valid on one common domain, with the common-policy error bounds. -/
229 theorem conditional_learning
230     (truth fitted : Ω → Model E A O) (U : Ω → Set (Model E A O))
231     (wf : ∀ ω,Witness V l (fitted ω))
232     (robust : ∀ ω m, m∈U ω → Nonempty (Witness V l m))
233     (event : Set Ω) (hmeas : MeasurableSet event) (δ : ℝ)
234     (hprob : 1-δ≤μ.real event) (hcover : ∀ ω∈event,truth ω∈U ω)
235     (ε : Ω → ℕ → ℝ) (e₀ : Ω → ℝ)
236     (herr : ∀ ω∈event,∀ t a z,z∈(finiteCone V l hn hs).base →
237       (finiteCone V l hn hs).discrepancy (fun o => (truth ω).1 (a,o))
238         (fun o => (fitted ω).1 (a,o)) z≤ε ω t)
239     (hinit : ∀ ω∈event,(finiteCone V l hn hs).value ((truth ω).2-(fitted ω).2)≤e₀ ω) :
240     MeasurableSet event ∧ 1-δ≤μ.real event ∧ ∀ ω∈event,
241       (∀ word,0≤l (wordAction (truth ω).1 word (truth ω).2) ∧
242         l (wordAction (truth ω).1 word (truth ω).2)≤1) ∧
243       (∀ word,0≤l (wordAction (fitted ω).1 word (fitted ω).2) ∧
244         l (wordAction (fitted ω).1 word (fitted ω).2)≤1) ∧
245       (∀ π,(∀ h,IsPrior (π h)) → ∀ n,
246         FiniteTV.distance (modelLaw V l hn hs π n (truth ω)) (modelLaw V l hn hs π n (fitted ω))≤
247           budget (e₀ ω) (ε ω) n ∧
248         FiniteTV.distance (observedLaw V l hn hs π n (truth ω)) (observedLaw V l hn hs π n (fitted ω))≤
249           budget (e₀ ω) (ε ω) n) := by
250   refine ⟨hmeas,hprob,?_⟩
251   intro ω hω
252   obtain ⟨wt⟩ := robust ω (truth ω) (hcover ω hω)
253   exact ⟨certified_all_words V l hn wt,certified_all_words V l hn (wf ω),
254     fun π hπ n => certified_policy_bounds V l hn hs wt (wf ω) (ε ω) (e₀ ω)
255       (herr ω hω) (hinit ω hω) π hπ n⟩
256 
257 omit [IsProbabilityMeasure μ] in
258 /-- The learner may select its finite generator set and common domain from the
259 data. Coverage is still stated on one explicit measurable event. -/
260 theorem conditional_selected_learning
261     {K : Ω → Type*} [∀ ω,Fintype (K ω)] [∀ ω,DecidableEq (K ω)]
262     (V₀ : ∀ ω,(K ω → ℝ) →ₗ[ℝ] E)
263     (hn₀ : ∀ ω,l.comp (V₀ ω)=FiniteInstruments.mass)
264     (hs₀ : ∀ ω,Function.Surjective (V₀ ω))
265     (truth fitted : Ω → Model E A O) (U : Ω → Set (Model E A O))
266     (wf : ∀ ω,Witness (V₀ ω) l (fitted ω))
267     (robust : ∀ ω m,m∈U ω → Nonempty (Witness (V₀ ω) l m))
268     (event : Set Ω) (hmeas : MeasurableSet event) (δ : ℝ)
269     (hprob : 1-δ≤μ.real event) (hcover : ∀ ω∈event,truth ω∈U ω)
270     (ε : Ω → ℕ → ℝ) (e₀ : Ω → ℝ)
271     (herr : ∀ ω∈event,∀ t a z,z∈(finiteCone (V₀ ω) l (hn₀ ω) (hs₀ ω)).base →
272       (finiteCone (V₀ ω) l (hn₀ ω) (hs₀ ω)).discrepancy
273         (fun o => (truth ω).1 (a,o)) (fun o => (fitted ω).1 (a,o)) z≤ε ω t)
274     (hinit : ∀ ω∈event,(finiteCone (V₀ ω) l (hn₀ ω) (hs₀ ω)).value
275       ((truth ω).2-(fitted ω).2)≤e₀ ω) :
276     MeasurableSet event ∧ 1-δ≤μ.real event ∧ ∀ ω∈event,
277       (∀ word,0≤l (wordAction (truth ω).1 word (truth ω).2) ∧
278         l (wordAction (truth ω).1 word (truth ω).2)≤1) ∧
279       (∀ word,0≤l (wordAction (fitted ω).1 word (fitted ω).2) ∧
280         l (wordAction (fitted ω).1 word (fitted ω).2)≤1) ∧
281       (∀ π,(∀ h,IsPrior (π h)) → ∀ n,
282         FiniteTV.distance
283           (modelLaw (V₀ ω) l (hn₀ ω) (hs₀ ω) π n (truth ω))
284           (modelLaw (V₀ ω) l (hn₀ ω) (hs₀ ω) π n (fitted ω))≤budget (e₀ ω) (ε ω) n ∧
285         FiniteTV.distance
286           (observedLaw (V₀ ω) l (hn₀ ω) (hs₀ ω) π n (truth ω))
287           (observedLaw (V₀ ω) l (hn₀ ω) (hs₀ ω) π n (fitted ω))≤budget (e₀ ω) (ε ω) n) := by
288   refine ⟨hmeas,hprob,?_⟩
289   intro ω hω
290   obtain ⟨wt⟩ := robust ω (truth ω) (hcover ω hω)
291   exact ⟨certified_all_words (V₀ ω) l (hn₀ ω) wt,
292     certified_all_words (V₀ ω) l (hn₀ ω) (wf ω),
293     fun π hπ n => certified_policy_bounds (V₀ ω) l (hn₀ ω) (hs₀ ω)
294       wt (wf ω) (ε ω) (e₀ ω) (herr ω hω) (hinit ω hω) π hπ n⟩
295 
296 end Confidence
297 section Atlas
298 open ConditionalStochasticCompletion
299 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
300 
301 /-- Exact atlas transport uses one conjugation and the transported mass row. -/
302 noncomputable def atlasModel (T : E ≃ₗ[ℝ] F) (m : Model E A O) : Model F A O :=
303   (atlasOperator T m.1,T m.2)
304 
305 omit [FiniteDimensional ℝ E] [DecidableEq J] in
306 include hn in
307 /-- The same finite coefficient prior stays normalized after coordinate transport. -/
308 theorem atlas_normalized (T : E ≃ₗ[ℝ] F) :
309     (atlasMass T l).comp (T.toLinearMap.comp V)=FiniteInstruments.mass := by
310   apply LinearMap.ext
311   intro a
312   change l (T.symm (T (V a)))=FiniteInstruments.mass a
313   rw [T.symm_apply_apply]
314   exact congrArg (fun L : (J → ℝ) →ₗ[ℝ] ℝ => L a) hn
315 
316 omit [FiniteDimensional ℝ E] [Fintype J] [DecidableEq J] in
317 include hs in
318 theorem atlas_surjective (T : E ≃ₗ[ℝ] F) : Function.Surjective (T.toLinearMap.comp V) :=
319   T.surjective.comp hs
320 
321 /-- Transport preserves the actual checked nonnegative matrices and initial
322 prior, rather than searching for another finite certificate. -/
323 noncomputable def atlasWitness (T : E ≃ₗ[ℝ] F) {m : Model E A O} (w : Witness V l m) :
324     Witness (T.toLinearMap.comp V) (atlasMass T l) (atlasModel T m) where
325   matrix := w.matrix
326   coefficients := w.coefficients
327   entries_nonnegative := w.entries_nonnegative
328   prior := w.prior
329   intertwines := by
330     intro s
331     apply LinearMap.ext
332     intro a
333     change T (m.1 s (T.symm (T (V a))))=T (V ((w.matrix s).mulVecLin a))
334     rw [T.symm_apply_apply]
335     exact congrArg T (congrArg (fun L : (J → ℝ) →ₗ[ℝ] E => L a) (w.intertwines s))
336   mass_law := by
337     intro a z
338     change (∑ o, l (T.symm (T (m.1 (a,o) (T.symm z)))) )=l (T.symm z)
339     simp only [T.symm_apply_apply]
340     exact w.mass_law a (T.symm z)
341   initial := by
342     change T m.2=T (V w.coefficients)
343     exact congrArg T w.initial
344 
345 omit [Fintype A] [Fintype O] [Fintype J] [DecidableEq J] [FiniteDimensional ℝ E] in
346 theorem atlas_word_probability (T : E ≃ₗ[ℝ] F) (m : Model E A O) (word : List (A × O)) :
347     atlasMass T l (wordAction (atlasModel T m).1 word (atlasModel T m).2)=
348       l (wordAction m.1 word m.2) :=
349   atlas_likelihood T m.1 l word m.2
350 
351 omit [Fintype A] [Fintype O] [Fintype J] [DecidableEq J] [FiniteDimensional ℝ E] in
352 /-- Full synthesis preserves every future experiment prediction, including
353 signed packets. The individual packets are not asserted to be probabilities. -/
354 theorem full_packet_prediction {K : Type*} [Fintype K]
355     (P : K → E →ₗ[ℝ] E) (hP : ∑ k,P k=LinearMap.id)
356     (m : Model E A O) (word : List (A × O)) (z : E) :
357     l (wordAction m.1 word (∑ k,P k z))=l (wordAction m.1 word z) :=
358   ConditionalStochasticCompletion.full_packet_prediction P hP m.1 l word z
359 
360 /-- Probability-mixture interpretation requires positivity of every packet.
361 That condition is separate from the synthesis identity. -/
362 theorem positive_packet_interpretation {K : Type*} [Fintype K] [DecidableEq K]
363     (P : K → E →ₗ[ℝ] E)
364     (hpos : ∀ k z,z∈(finiteCone V l hn hs).carrier → P k z∈(finiteCone V l hn hs).carrier)
365     (hP : ∑ k,P k=LinearMap.id) (z : E) (hz : z∈(finiteCone V l hn hs).base) :
366     (∑ k,l (P k z)=1) ∧
367     (∑ k∈Finset.univ.filter (fun k => 0<l (P k z)),
368       l (P k z) • ((l (P k z))⁻¹ • P k z))=z := by
369   let C := finiteCone V l hn hs
370   exact ⟨PositivePackets.packet_weights_sum l P hP z hz.2,
371     PositivePackets.positive_packet_mixture C.carrier l
372       (fun x hx hne => C.mass_pos hx hne) P hpos hP z hz.1⟩
373 
374 /-- An individual normalized packet is a probability state only under its
375 explicit cone-positivity and positive-mass hypotheses. -/
376 theorem positive_packet_state (P : E →ₗ[ℝ] E)
377     (hpos : ∀ z,z∈(finiteCone V l hn hs).carrier → P z∈(finiteCone V l hn hs).carrier)
378     (z : E) (hz : z∈(finiteCone V l hn hs).base) (hp : 0<l (P z)) :
379     (l (P z))⁻¹ • P z∈(finiteCone V l hn hs).base := by
380   let C := finiteCone V l hn hs
381   exact PositivePackets.normalized_packet C.carrier
382     (fun a ha x hx => C.smul_mem ha hx) l P hpos z hz.1 hp
383 
384 end Atlas
385 
386 section Observable
387 open Behavior
388 variable {I : Type*} [Fintype I] [DecidableEq I]
389 variable (f : List (A × O) → ℝ) [FiniteDimensional ℝ (space f)]
390 variable (tests histories : I → List (A × O))
391 variable (hH : IsUnit (core f tests histories).det)
392 variable (hr : Module.finrank ℝ (space f)≤Fintype.card I) (i₀ : I) (hi : tests i₀=[])
393 
394 /-- The true operator/initial pair is the actual observable population-table
395 construction of P37, not an unknown hidden-state model supplied to a learner. -/
396 noncomputable def observableModel : Model (I → ℝ) A O :=
397   ((tableModel f tests histories hH hr i₀ hi).operator,
398    (tableModel f tests histories hH hr i₀ hi).initial)
399 
400 omit [Fintype A] [Fintype O] in
401 /-- This is the exact full-process likelihood represented by that constructed pair. -/
402 theorem observable_word_probability (word : List (A × O)) :
403     (LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ) (wordAction (observableModel f tests histories hH hr i₀ hi).1 word
404       (observableModel f tests histories hH hr i₀ hi).2)=f word :=
405   (tableModel f tests histories hH hr i₀ hi).correct word
406 
407 omit [Fintype A] [Fintype O] in
408 include hH hr in
409 /-- The observable state dimension is minimal among actual finite realizations. -/
410 theorem observable_minimal {F : Type*} [AddCommGroup F] [Module ℝ F]
411     [FiniteDimensional ℝ F] (r : Behavior.Realization f F) :
412     Fintype.card I≤Module.finrank ℝ F :=
413   tableModel_minimal f tests histories hH hr r
414 
415 omit [Fintype A] in
416 /-- A finite certificate for the reconstructed observable pair certifies the
417 actual process word laws, and not merely the table entries used to construct it. -/
418 theorem observable_certificate_all_words
419     {K : Type*} [Fintype K] [DecidableEq K]
420     (V₀ : (K → ℝ) →ₗ[ℝ] (I → ℝ))
421     (hn₀ : (LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ).comp V₀=FiniteInstruments.mass)
422     (w : Witness V₀ (LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ) (observableModel f tests histories hH hr i₀ hi)) :
423     ∀ word,0≤f word ∧ f word≤1 := by
424   intro word
425   have hw := certified_all_words V₀ (LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ) hn₀ w word
426   rwa [observable_word_probability f tests histories hH hr i₀ hi] at hw
427 
428 omit [Fintype A] in
429 /-- P37 reachability discharges the full-row-rank requirement for every true
430 observable-model witness. -/
431 theorem observable_witness_surjective
432     {K : Type*} [Fintype K] [DecidableEq K]
433     (V₀ : (K → ℝ) →ₗ[ℝ] (I → ℝ))
434     (w : Witness V₀ (LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ)
435       (observableModel f tests histories hH hr i₀ hi)) : Function.Surjective V₀ :=
436   witness_surjective_of_reachable V₀ (LinearMap.proj i₀)
437     (tableModel f tests histories hH hr i₀ hi)
438     (tableModel_reachable f tests histories hH hr i₀ hi) w
439 
440 section ObservableConfidence
441 open MeasureTheory
442 variable {Ω K : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
443 variable [Fintype K] [DecidableEq K]
444 
445 /-- The same confidence-and-certificate implication with the true model fixed
446 literally to P37's population-table reconstruction. It connects the observable
447 process law, not merely a generic matrix family, to the all-horizon bound. -/
448 theorem conditional_observable_learning
449     (V₀ : (K → ℝ) →ₗ[ℝ] (I → ℝ))
450     (hn₀ : (LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ).comp V₀=FiniteInstruments.mass)
451     (hs₀ : Function.Surjective V₀)
452     (fitted : Ω → Model (I → ℝ) A O) (U : Ω → Set (Model (I → ℝ) A O))
453     (wf : ∀ ω,Witness V₀ (LinearMap.proj i₀) (fitted ω))
454     (robust : ∀ ω m,m∈U ω → Nonempty (Witness V₀ (LinearMap.proj i₀) m))
455     (event : Set Ω) (hmeas : MeasurableSet event) (δ : ℝ)
456     (hprob : 1-δ≤μ.real event)
457     (hcover : ∀ ω∈event,observableModel f tests histories hH hr i₀ hi∈U ω)
458     (ε : Ω → ℕ → ℝ) (e₀ : Ω → ℝ)
459     (herr : ∀ ω∈event,∀ t a z,z∈(finiteCone V₀ (LinearMap.proj i₀) hn₀ hs₀).base →
460       (finiteCone V₀ (LinearMap.proj i₀) hn₀ hs₀).discrepancy
461         (fun o => (observableModel f tests histories hH hr i₀ hi).1 (a,o))
462         (fun o => (fitted ω).1 (a,o)) z≤ε ω t)
463     (hinit : ∀ ω∈event,(finiteCone V₀ (LinearMap.proj i₀) hn₀ hs₀).value
464       ((observableModel f tests histories hH hr i₀ hi).2-(fitted ω).2)≤e₀ ω) :
465     (∀ word,(LinearMap.proj i₀ : (I → ℝ) →ₗ[ℝ] ℝ)
466       (wordAction (observableModel f tests histories hH hr i₀ hi).1 word
467         (observableModel f tests histories hH hr i₀ hi).2)=f word) ∧
468     MeasurableSet event ∧ 1-δ≤μ.real event ∧ ∀ ω∈event,
469       (∀ word,0≤f word ∧ f word≤1) ∧
470       (∀ π,(∀ h,IsPrior (π h)) → ∀ n,
471         FiniteTV.distance (modelLaw V₀ (LinearMap.proj i₀) hn₀ hs₀ π n
472           (observableModel f tests histories hH hr i₀ hi))
473           (modelLaw V₀ (LinearMap.proj i₀) hn₀ hs₀ π n (fitted ω))≤budget (e₀ ω) (ε ω) n ∧
474         FiniteTV.distance (observedLaw V₀ (LinearMap.proj i₀) hn₀ hs₀ π n
475           (observableModel f tests histories hH hr i₀ hi))
476           (observedLaw V₀ (LinearMap.proj i₀) hn₀ hs₀ π n (fitted ω))≤budget (e₀ ω) (ε ω) n) := by
477   refine ⟨observable_word_probability f tests histories hH hr i₀ hi,hmeas,hprob,?_⟩
478   intro ω hω
479   obtain ⟨wt⟩ := robust ω _ (hcover ω hω)
480   refine ⟨observable_certificate_all_words f tests histories hH hr i₀ hi V₀ hn₀ wt,?_⟩
481   intro π hπ n
482   exact certified_policy_bounds V₀ (LinearMap.proj i₀) hn₀ hs₀ wt (wf ω) (ε ω) (e₀ ω)
483     (herr ω hω) (hinit ω hω) π hπ n
484 
485 end ObservableConfidence
486 
487 end Observable
488 
489 end Komorebi.LSM.CertificateLearning

Back to source controls