StrictRationalSearch.lean

1 import KomorebiLSM.StrictRationalGeometry
2 import KomorebiLSM.BernsteinGridSearch
3 import KomorebiLSM.ConvexMargin
4 import Mathlib.Data.Rat.Encodable
5 
6 set_option autoImplicit false
7 namespace Komorebi.LSM.StrictRationalSearch
8 open scoped BigOperators Matrix
9 open LorentzCylinder RobustOrientedMargin RationalTransform
10 open TensorBernsteinCertificate RationalBernsteinMargin RationalBernsteinTermination
11 open BernsteinGridSearch StrictRationalGeometry
12 noncomputable section
13 
14 /-- A complete finite description: rational affine transform, margin, common depth and all grid arrays. -/
15 abbrev Candidate (nf na : ℕ) := Parameters ℚ × ℚ × Σ N : ℕ,
16   Fin nf → Fin na → Bool → Bool → GridData N
17 
18 instance candidateEncodable (nf na : ℕ) : Encodable (Candidate nf na) := by
19   unfold Candidate Parameters
20   infer_instance
21 
22 variable {nf na ni n : ℕ}
23 def transform (c : Candidate nf na) : RationalTransform.RationalMatrix := affineMatrix c.1
24 def margin (c : Candidate nf na) : ℚ := c.2.1
25 def depth (c : Candidate nf na) : ℕ := c.2.2.1
26 def grids (c : Candidate nf na) := c.2.2.2
27 
28 def Valid (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
29     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) : Prop :=
30   (transform c).det≠0 ∧ 0<margin c ∧
31   (∀ j,StrictVector (transform c *ᵥ z j)) ∧
32   ∀ i a which left, gridValid
33     (testPolynomial (rationalConjugated (transform c) (G i a)) (margin c) which left)
34     square (depth c) (grids c i a which left)
35 
36 /-- Every submitted test is a finite rational sign or finitely supported polynomial comparison. -/
37 instance decidableValid (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
38     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) : Decidable (Valid G z c) := by
39   rcases c with ⟨q,kappa,N,d⟩
40   unfold Valid transform margin depth grids StrictVector
41   dsimp only
42   infer_instance
43 
44 def certificate (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
45     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) (i : Fin nf) (a : Fin na) :
46     Certificate (rationalConjugated (transform c) (G i a)) (margin c) where
47   orientationWitness left :=
48     (toUniform _ _ (grids c i a false left) (h.2.2.2 i a false left)).toSubdivision
49   squareGapWitness left :=
50     (toUniform _ _ (grids c i a true left) (h.2.2.2 i a true left)).toSubdivision
51 
52 theorem candidate_exists (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
53     (z : Fin ni → Fin 3 → ℚ) (T : RealMatrix) (hT : IsUnit T.det) (hmass : MassPreserving T)
54     (hinit : ∀ j,0<slack (operator T (rationalState (z j)))) (eta : ℝ) (heta : 0<eta)
55     (hmargin : ∀ i a u,u∈Set.Icc (-1 : ℝ) 1 → eta≤sigma (conjugated T (G i a) u)) :
56     ∃ c : Candidate nf na, Valid G z c := by
57   obtain ⟨q,kappa,hk,hq,hi,hm⟩ := rational_strict_sector G (fun j => rationalState (z j))
58     T hT hmass hinit eta heta hmargin
59   have hcombined : ∀ ia : Fin nf × Fin na, ∀ u, u∈Set.Icc (-1 : ℝ) 1 →
60       (kappa : ℝ)<sigma (PolynomialGram.operatorPolynomial
61         (fun k => RationalBernsteinMargin.matrixOperator (rationalConjugated (affineMatrix q) (G ia.1 ia.2) k)) u) :=
62     fun ia => hm ia.1 ia.2
63   obtain ⟨N,hN⟩ := strict_family_eventual
64     (fun ia : Fin nf × Fin na => rationalConjugated (affineMatrix q) (G ia.1 ia.2)) kappa hcombined
65   let c : Candidate nf na := ⟨q,kappa,N,fun i a which left =>
66     ofUniform (hN N le_rfl (i,a) which left).some⟩
67   refine ⟨c,isUnit_iff_ne_zero.mp hq,hk,?_,?_⟩
68   · intro j
69     rw [strictVector_iff_slack,← operator_rationalState]
70     exact hi j
71   · intro i a which left
72     exact ofUniform_valid (hN N le_rfl (i,a) which left).some
73 
74 /-- This formal semidecision uses the explicit finite checker, not an existence oracle.
75 Mathlib's polynomial representation is noncomputable; no Lean-VM extraction is claimed. -/
76 def search (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
77     (z : Fin ni → Fin 3 → ℚ) : ℕ → Option (Candidate nf na) :=
78   BernsteinGridSearch.search (Valid G z)
79 
80 theorem search_sound (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
81     (z : Fin ni → Fin 3 → ℚ) (budget : ℕ) (c : Candidate nf na)
82     (h : search G z budget=some c) : Valid G z c :=
83   BernsteinGridSearch.search_sound _ h
84 
85 /-- A strict actual real sector gives a finite search stage and a stable sound return thereafter. -/
86 theorem conditional_search (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
87     (z : Fin ni → Fin 3 → ℚ) (T : RealMatrix) (hT : IsUnit T.det) (hmass : MassPreserving T)
88     (hinit : ∀ j,0<slack (operator T (rationalState (z j)))) (eta : ℝ) (heta : 0<eta)
89     (hmargin : ∀ i a u,u∈Set.Icc (-1 : ℝ) 1 → eta≤sigma (conjugated T (G i a) u)) :
90     ∃ budget c, Valid G z c ∧ ∀ b,budget≤b → search G z b=some c :=
91   BernsteinGridSearch.search_eventually _
92     (candidate_exists G z T hT hmass hinit eta heta hmargin)
93 
94 /-- These are the supplied complete families under the returned actual rational similarity. -/
95 def families (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
96     (c : Candidate nf na) : Fin nf → ConvexMargin.Family (Fin na) n ℂ :=
97   fun i a k => RationalBernsteinMargin.matrixOperator (rationalConjugated (transform c) (G i a) k)
98 
99 def initials (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) : Fin ni → State ℂ :=
100   fun j => operator (castMatrix (transform c)) (rationalState (z j))
101 
102 theorem valid_unit (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
103     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) : IsUnit (transform c).det :=
104   isUnit_iff_ne_zero.mpr h.1
105 
106 theorem transform_mass (c : Candidate nf na) : MassPreserving (castMatrix (transform c)) := by
107   change MassPreserving (castMatrix (affineMatrix c.1))
108   rw [← affineMatrix_cast]
109   exact affineMatrix_mass _
110 
111 /-- The fixed input families retain their independently checked exact integrated mass. -/
112 def OriginalMass (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix) : Prop :=
113   ∀ i a y, ((∑ k : Fin n,UniformIntervalMoments.moment k • operator (castMatrix (G i a k))) y).1=y.1
114 
115 theorem valid_feasible (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
116     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) (hm : OriginalMass G)
117     (i : Fin nf) : families G c i∈ConvexMargin.feasible (fun _ _ => (margin c : ℝ)) := by
118   constructor
119   · intro a u hu
120     exact (certificate G z c h i a).margin u hu
121   · intro a y
122     change ((∑ k : Fin n,UniformIntervalMoments.moment k • families G c i a k) y).1=y.1
123     simp only [families,rational_conjugated_coefficient (transform c) (valid_unit G z c h)]
124     exact conjugate_mass _ (unit_castMatrix _ (valid_unit G z c h)) (transform_mass c)
125       (fun k => operator (castMatrix (G i a k))) (fun k => UniformIntervalMoments.moment k) (hm i a) y
126 
127 theorem valid_initial (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
128     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c)
129     (hz : ∀ j,z j 0=1) (j : Fin ni) : initials z c j∈(probabilityCone (V := ℂ)).base := by
130   have hp := (strictVector_iff_slack _).mp (h.2.2.1 j)
131   rw [← operator_rationalState] at hp
132   refine ⟨?_,?_⟩
133   · change ‖(initials z c j).2‖≤(initials z c j).1
134     change 0<(initials z c j).1-‖(initials z c j).2‖ at hp
135     linarith
136   · change (operator (castMatrix (transform c)) (rationalState (z j))).1=1
137     rw [mass_preserving_operator _ (transform_mass c)]
138     change (z j 0 : ℝ)=1
139     exact_mod_cast hz j
140 
141 /-- Every returned complete-family convex combination is an actual density instrument. -/
142 def hullInstrument (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
143     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) (hm : OriginalMass G)
144     (F : ConvexMargin.Family (Fin na) n ℂ) (hF : F∈convexHull ℝ (Set.range (families G c))) :
145     ContinuousInstrument.DensityInstrument (A := Fin na) (probabilityCone (V := ℂ)) UniformIntervalMoments.measure :=
146   ConvexMargin.instrument (fun _ _ => (margin c : ℝ)) F
147     (ConvexMargin.hull_feasible (families G c) _ (valid_feasible G z c h hm) hF)
148     (fun _ _ _ => by exact_mod_cast h.2.1.le)
149 
150 /-- Complete operator and initial convex hulls use independent coefficients and have all-horizon laws. -/
151 theorem returned_hull_probability (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
152     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) (hm : OriginalMass G)
153     (hz : ∀ j,z j 0=1) (F : ConvexMargin.Family (Fin na) n ℂ)
154     (hF : F∈convexHull ℝ (Set.range (families G c)))
155     (y : State ℂ) (hy : y∈convexHull ℝ (Set.range (initials z c)))
156     (policy : ContinuousRecords.Policy (A := Fin na) (Y := ℝ)) (N : ℕ) :
157     MeasureTheory.IsProbabilityMeasure (ContinuousRecords.recordLaw
158       (hullInstrument G z c h hm F hF) policy y N) :=
159   ContinuousRecords.recordLaw_probability _ policy
160     ⟨y,ConvexMargin.hull_initial (initials z c) (valid_initial G z c h hz) hy⟩ N
161 
162 /-- The complete conditional result connects the same returned finite description to actual hull laws. -/
163 theorem conditional_search_with_hulls
164     (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
165     (z : Fin ni → Fin 3 → ℚ) (hm : OriginalMass G) (hz : ∀ j,z j 0=1)
166     (T : RealMatrix) (hT : IsUnit T.det) (hmass : MassPreserving T)
167     (hinit : ∀ j,0<slack (operator T (rationalState (z j)))) (eta : ℝ) (heta : 0<eta)
168     (hmargin : ∀ i a u,u∈Set.Icc (-1 : ℝ) 1 → eta≤sigma (conjugated T (G i a) u)) :
169     ∃ (budget : ℕ) (c : Candidate nf na) (h : Valid G z c),
170       (∀ b,budget≤b → search G z b=some c) ∧
171       ∀ (F : ConvexMargin.Family (Fin na) n ℂ)
172         (hF : F∈convexHull ℝ (Set.range (families G c)))
173         (y : State ℂ) (_hy : y∈convexHull ℝ (Set.range (initials z c)))
174         (policy : ContinuousRecords.Policy (A := Fin na) (Y := ℝ)) (N : ℕ),
175         MeasureTheory.IsProbabilityMeasure (ContinuousRecords.recordLaw
176           (hullInstrument G z c h hm F hF) policy y N) := by
177   obtain ⟨budget,c,h,hstable⟩ := conditional_search G z T hT hmass hinit eta heta hmargin
178   exact ⟨budget,c,h,hstable,returned_hull_probability G z c h hm hz⟩
179 
180 /-- The same coordinate change acts linearly on every complete real coefficient family. -/
181 def transformFamily (T : RealMatrix) : ConvexMargin.Family (Fin na) n ℂ →ₗ[ℝ]
182     ConvexMargin.Family (Fin na) n ℂ where
183   toFun F a k := conjugate T (F a k)
184   map_add' F H := by
185     funext a k
186     apply ContinuousLinearMap.ext
187     intro y
188     simp [conjugate]
189   map_smul' r F := by
190     funext a k
191     apply ContinuousLinearMap.ext
192     intro y
193     simp [conjugate]
194 
195 def sourceFamilies (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix) :
196     Fin nf → ConvexMargin.Family (Fin na) n ℂ := fun i a k => operator (castMatrix (G i a k))
197 
198 def sourceInitials (z : Fin ni → Fin 3 → ℚ) : Fin ni → State ℂ := fun j => rationalState (z j)
199 
200 theorem source_hull_mapped (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
201     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c)
202     (F : ConvexMargin.Family (Fin na) n ℂ) (hF : F∈convexHull ℝ (Set.range (sourceFamilies G))) :
203     transformFamily (castMatrix (transform c)) F∈convexHull ℝ (Set.range (families G c)) := by
204   let L := transformFamily (castMatrix (transform c)) (na := na) (n := n)
205   have himage : L F∈convexHull ℝ (L '' Set.range (sourceFamilies G)) := by
206     rw [← L.image_convexHull]
207     exact ⟨F,hF,rfl⟩
208   have heq : (fun i => L (sourceFamilies G i)) = families G c := by
209     funext i a k
210     exact (rational_conjugated_coefficient (transform c) (valid_unit G z c h) (G i a) k).symm
211   rw [← Set.range_comp',heq] at himage
212   exact himage
213 
214 theorem source_initial_hull_mapped (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na)
215     (y : State ℂ) (hy : y∈convexHull ℝ (Set.range (sourceInitials z))) :
216     operator (castMatrix (transform c)) y∈convexHull ℝ (Set.range (initials z c)) := by
217   let L := (operator (castMatrix (transform c))).toLinearMap
218   have himage : L y∈convexHull ℝ (L '' Set.range (sourceInitials z)) := by
219     rw [← L.image_convexHull]
220     exact ⟨y,hy,rfl⟩
221   rw [← Set.range_comp'] at himage
222   change operator (castMatrix (transform c)) y∈convexHull ℝ (Set.range (initials z c)) at himage
223   exact himage
224 
225 theorem source_family_action (T : RealMatrix) (hT : IsUnit T.det)
226     (F : ConvexMargin.Family (Fin na) n ℂ) (a : Fin na) (u : ℝ) (y : State ℂ) :
227     operator T (PolynomialGram.operatorPolynomial (F a) u y) =
228       PolynomialGram.operatorPolynomial ((transformFamily T F) a) u (operator T y) := by
229   have he : operator T⁻¹ (operator T y)=y := (atlas T hT).symm_apply_apply y
230   change operator T (PolynomialGram.operatorPolynomial (F a) u y) =
231     PolynomialGram.operatorPolynomial (fun k => conjugate T (F a k)) u (operator T y)
232   simp only [PolynomialGram.operatorPolynomial,sum_apply,smul_apply,map_sum,map_smul]
233   apply Finset.sum_congr rfl
234   intro k _
235   apply congrArg (fun w : State ℂ => u^(k : ℕ) • w)
236   change operator T (F a k y) = operator T (F a k (operator T⁻¹ (operator T y)))
237   rw [he]
238 
239 /-- Soundness applies to the original supplied-family hull in the returned actual atlas domain. -/
240 theorem source_hull_preserves (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
241     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) (hm : OriginalMass G)
242     (F : ConvexMargin.Family (Fin na) n ℂ) (hF : F∈convexHull ℝ (Set.range (sourceFamilies G)))
243     (a : Fin na) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) (y : State ℂ)
244     (hy : y∈(atlasCone (atlas (castMatrix (transform c)) (unit_castMatrix _ (valid_unit G z c h)))).carrier) :
245     PolynomialGram.operatorPolynomial (F a) u y∈
246       (atlasCone (atlas (castMatrix (transform c)) (unit_castMatrix _ (valid_unit G z c h)))).carrier := by
247   have hFh := source_hull_mapped G z c h F hF
248   have hf := ConvexMargin.hull_feasible (families G c) (fun _ _ => (margin c : ℝ))
249     (valid_feasible G z c h hm) hFh
250   change operator (castMatrix (transform c)) (PolynomialGram.operatorPolynomial (F a) u y)∈cone
251   rw [source_family_action _ (unit_castMatrix _ (valid_unit G z c h))]
252   apply preserves_of_normalized _ _ hy
253   intro v hv
254   have hs := (hf.1 a u hu).trans (sigma_le _ v hv)
255   have hk : (0 : ℝ)<margin c := by exact_mod_cast h.2.1
256   change ‖(PolynomialGram.operatorPolynomial ((transformFamily (castMatrix (transform c)) F) a) u (1,v)).2‖≤_
257   change (margin c : ℝ)≤
258     (PolynomialGram.operatorPolynomial ((transformFamily (castMatrix (transform c)) F) a) u (1,v)).1-
259       ‖(PolynomialGram.operatorPolynomial ((transformFamily (castMatrix (transform c)) F) a) u (1,v)).2‖ at hs
260   linarith
261 
262 theorem source_hull_initial_domain (G : Fin nf → Fin na → Fin n → RationalTransform.RationalMatrix)
263     (z : Fin ni → Fin 3 → ℚ) (c : Candidate nf na) (h : Valid G z c) (hz : ∀ j,z j 0=1)
264     (y : State ℂ) (hy : y∈convexHull ℝ (Set.range (sourceInitials z))) :
265     y∈(atlasCone (atlas (castMatrix (transform c)) (unit_castMatrix _ (valid_unit G z c h)))).base := by
266   have hi := ConvexMargin.hull_initial (initials z c) (valid_initial G z c h hz)
267     (source_initial_hull_mapped z c y hy)
268   exact hi
269 
270 end
271 end Komorebi.LSM.StrictRationalSearch

Back to source controls