ContinuousRealizationP61.lean

1 import KomorebiLSM.ContinuousPopulationBridge
2 import KomorebiLSM.ContinuousBinnedRecords
3 import KomorebiLSM.PositiveCellP58
4 import KomorebiLSM.ContinuousTV
5 import KomorebiLSM.PositivePackets
6 
7 /-! P61: the same population-reconstructed polynomial coefficients are used
8 by the finite matrix/Gram instrument, exact coordinate and packet identities,
9 bin-history event model, positive cell approximation and common-policy budget.
10 Dimension, degree, initial admissibility and approximation inputs stay explicit. -/
11 set_option autoImplicit false
12 namespace Komorebi.LSM.ContinuousRealizationP61
13 open ContinuousPopulationBridge MeasureTheory ProbabilityTheory
14 open scoped BigOperators Matrix
15 
16 variable {r degree : ℕ} {A D R : Type*}
17 variable [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
18 variable [Fintype D] [DecidableEq D] [Fintype R]
19 
20 /-- The instrument uses the actual inverse-moment fitted coefficients, not
21 an unrelated model supplied alongside the population reconstruction. -/
22 noncomputable def realizedInstrument (T S : Operator r)
23     (C : A → Fin (degree+1) → Operator r)
24     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
25     {q bound : ℕ}
26     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J
27       (fittedCoefficients T S C) q bound) :
28     ContinuousInstrument.DensityInstrument (A := A) M.coneInstance UniformIntervalMoments.measure :=
29   PolynomialGramP53.instrument M b (fittedCoefficients T S C) W
30 
31 /-- The mass-row equality is the checked coordinate readout identity. Exact
32 population reconstruction and the independent finite Gram witness then give
33 the full represented density and actual all-horizon probability laws. -/
34 theorem population_realization_certificate (T S : Operator r)
35     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
36     (C : A → Fin (degree+1) → Operator r)
37     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
38     {q bound : ℕ}
39     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J
40       (fittedCoefficients T S C) q bound)
41     (l : State r →ₗ[ℝ] ℝ) (hmass : M.mass.comp T.mulVecLin=l)
42     (z₀ : State r) (hinitial : (M.J (T *ᵥ z₀)).PosSemidef ∧ M.mass (T *ᵥ z₀)=1) :
43     let I := realizedInstrument T S C M b W
44     (∀ a k,fittedCoefficients T S C a k=matrixCLM (T * C a k * T⁻¹)) ∧
45     (∀ a u x,I.op a u x=(T * FiniteMomentIdentification.density (C a) u * T⁻¹) *ᵥ x) ∧
46     (∀ word : List (A × ℝ),M.mass (FiniteInstruments.wordAction
47       (fun s : A × ℝ => (I.op s.1 s.2).toLinearMap) word (T *ᵥ z₀))=
48         l (FiniteMomentIdentification.wordState (fun a => FiniteMomentIdentification.density (C a)) word z₀)) ∧
49     l z₀=1 ∧
50     (∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ x∈M.cone,I.op a u x∈M.cone) ∧
51     (∀ a,IsMarkovKernel (I.kernel a)) ∧
52     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ N,
53       IsProbabilityMeasure (ContinuousRecords.recordLaw I π (T *ᵥ z₀) N)) ∧
54     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ),∀ N,
55       (ContinuousRecords.recordLaw I π (T *ᵥ z₀) (N+1)).fst=
56         ContinuousRecords.recordLaw I π (T *ᵥ z₀) N) ∧
57     (∀ actions : ℕ → A,∀ N,
58       IsProbabilityMeasure (ContinuousRecords.observationLaw I actions (T *ᵥ z₀) N)) ∧
59     (∀ actions : ℕ → A,∀ N (event : Set (ContinuousRecords.History ℝ N)),MeasurableSet event →
60       ContinuousRecords.observationLaw I actions (T *ᵥ z₀) N event=
61         ∫⁻ h in event,ENNReal.ofReal (M.mass (ContinuousRecords.observationRun I actions (T *ᵥ z₀) N h))
62           ∂ContinuousRecords.reference UniformIntervalMoments.measure N) := by
63   dsimp only
64   let I := realizedInstrument T S C M b W
65   have hb : T *ᵥ z₀∈M.coneInstance.base := hinitial
66   refine ⟨fitted_coefficient_identification T S hcore C,?_,?_,?_,?_,?_,?_,?_,?_,?_⟩
67   · intro a u x
68     change PolynomialGram.operatorPolynomial (fittedCoefficients T S C a) u x=_
69     rw [fitted_density_identification T S hcore,matrixCLM_apply]
70   · intro word
71     exact fitted_word_likelihood T S hcore C l M.mass hmass word z₀
72   · have he := congrArg (fun L : State r →ₗ[ℝ] ℝ => L z₀) hmass
73     exact he.symm.trans hinitial.2
74   · intro a u hu x hx
75     exact W.positive a u hu x hx
76   · intro a
77     infer_instance
78   · intro π N
79     exact ContinuousRecords.recordLaw_probability I π ⟨T *ᵥ z₀,hb⟩ N
80   · intro π N
81     exact ContinuousRecords.recordLaw_consistent I π hb.1 N
82   · intro actions N
83     exact ContinuousRecords.observationLaw_probability I actions ⟨T *ᵥ z₀,hb⟩ N
84   · intro actions N event hEvent
85     exact ContinuousRecords.observationLaw_product_density I actions (T *ᵥ z₀) N event hEvent
86 
87 section OriginalCoordinates
88 
89 /-- Transporting the independently checked fitted certificate back by the
90 population-derived inverse atlas constructs an instrument with the literal
91 original coefficient family. It is not an assumed generating-law equality. -/
92 noncomputable def originalInstrument (T S : Operator r)
93     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
94     (C : A → Fin (degree+1) → Operator r)
95     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
96     {q bound : ℕ}
97     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J (fittedCoefficients T S C) q bound) :
98     ContinuousInstrument.DensityInstrument (A := A)
99       (M.transport (populationEquiv T S hcore).symm).coneInstance UniformIntervalMoments.measure :=
100   CertifiedTemplate.fittedInstrument M b (fittedCoefficients T S C) (originalCoefficients C) W
101     (populationEquiv T S hcore).symm (population_inverse_coefficient_match T S hcore C)
102 
103 omit [MeasurableSpace A] [MeasurableSingletonClass A] in
104 theorem original_instrument_op (T S : Operator r)
105     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
106     (C : A → Fin (degree+1) → Operator r)
107     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
108     {q bound : ℕ}
109     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J (fittedCoefficients T S C) q bound)
110     (a : A) (u : ℝ) (x : State r) :
111     (originalInstrument T S hcore C M b W).op a u x=
112       FiniteMomentIdentification.density (C a) u *ᵥ x := by
113   change PolynomialGram.operatorPolynomial (fun k => matrixCLM (C a k)) u x=_
114   rw [polynomial_matrix_density,matrixCLM_apply]
115 
116 omit [DecidableEq D] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
117 theorem original_instrument_mass (T S : Operator r)
118     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
119     (M : MatrixEmbedding.Embedding (State r) D)
120     (l : State r →ₗ[ℝ] ℝ) (hmass : M.mass.comp T.mulVecLin=l) :
121     (M.transport (populationEquiv T S hcore).symm).mass=l := by
122   apply LinearMap.ext
123   intro x
124   change M.mass (T *ᵥ x)=l x
125   exact congrArg (fun L : State r →ₗ[ℝ] ℝ => L x) hmass
126 
127 omit [MeasurableSingletonClass A] in
128 /-- The complete actual record measures of the original declared polynomial
129 family and the certified reconstructed family coincide in their own atlases. -/
130 theorem population_record_law (T S : Operator r)
131     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
132     (C : A → Fin (degree+1) → Operator r)
133     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
134     {q bound : ℕ}
135     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J (fittedCoefficients T S C) q bound)
136     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (z₀ : State r) (N : ℕ) :
137     ContinuousRecords.recordLaw (originalInstrument T S hcore C M b W) π z₀ N=
138       ContinuousRecords.recordLaw (realizedInstrument T S C M b W) π (T *ᵥ z₀) N := by
139   have h := CertifiedTemplate.record_law_transport M b (fittedCoefficients T S C)
140     (originalCoefficients C) W (populationEquiv T S hcore).symm
141     (population_inverse_coefficient_match T S hcore C) π (populationEquiv T S hcore z₀) N
142   rw [LinearEquiv.symm_apply_apply] at h
143   simpa only [originalInstrument,realizedInstrument,populationEquiv_apply] using h
144 
145 end OriginalCoordinates
146 
147 section Template
148 variable (T S : Operator r) (C : A → Fin (degree+1) → Operator r)
149 variable (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
150 variable (template : A → Fin (degree+1) → State r →L[ℝ] State r)
151 variable {q bound : ℕ} (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J template q bound)
152 variable (U : State r ≃ₗ[ℝ] State r) (lhat : State r →ₗ[ℝ] ℝ)
153 variable (hm : CertifiedTemplate.Matches
154   (fun s : A × Fin (degree+1) => (template s.1 s.2).toLinearMap)
155   (fun s : A × Fin (degree+1) => (fittedCoefficients T S C s.1 s.2).toLinearMap)
156   M.mass lhat U.toLinearMap)
157 
158 /-- A successful fixed-template linear match constructs a finite certificate
159 for precisely the population-fitted coefficient family used above. -/
160 noncomputable def recognizedPopulationCertificate :
161     PolynomialGram.CoefficientCertificate (b.map U) (M.transport U).coneInstance (M.transport U).J
162       (fittedCoefficients T S C) q bound :=
163   CertifiedTemplate.transportedCertificate M b template (fittedCoefficients T S C) W U
164     (fun a k x => hm.coefficient_apply (a,k) x)
165 
166 /-- The matching constructor keeps the independent initial-state test. The
167 same population initial test vector is used in the actual fitted law. -/
168 theorem recognized_population_probability (z₀ : State r)
169     (hinitial : (M.J (U.symm (T *ᵥ z₀))).PosSemidef ∧ lhat (T *ᵥ z₀)=1)
170     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (N : ℕ) :
171     IsProbabilityMeasure (ContinuousRecords.recordLaw
172       (realizedInstrument T S C (M.transport U) (b.map U)
173         (recognizedPopulationCertificate T S C M b template W U lhat hm)) π (T *ᵥ z₀) N) :=
174   CertifiedTemplate.fitted_record_probability M b template (fittedCoefficients T S C) W U
175     (fun a k x => hm.coefficient_apply (a,k) x) lhat hm.2 (T *ᵥ z₀) hinitial π N
176 
177 end Template
178 
179 section Atlas
180 
181 /-- Exact atlas transport is defined by conjugation of the actual fitted
182 coefficients; no all-word or event-law equality is a hypothesis. -/
183 noncomputable def atlasCoefficients {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
184     [FiniteDimensional ℝ E] {n : ℕ} (U : E ≃ₗ[ℝ] E)
185     (B : A → Fin n → E →L[ℝ] E) (a : A) (k : Fin n) : E →L[ℝ] E :=
186   U.toContinuousLinearEquiv.toContinuousLinearMap.comp
187     ((B a k).comp U.symm.toContinuousLinearEquiv.toContinuousLinearMap)
188 
189 omit [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A] in
190 theorem atlas_coefficient_match {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
191     [FiniteDimensional ℝ E] {n : ℕ} (U : E ≃ₗ[ℝ] E)
192     (B : A → Fin n → E →L[ℝ] E) (a : A) (k : Fin n) (x : E) :
193     atlasCoefficients U B a k (U x)=U (B a k x) := by
194   simp [atlasCoefficients]
195 
196 omit [MeasurableSingletonClass A] in
197 /-- The actual full common-policy event measures are invariant under an exact
198 atlas. The transported finite Gram certificate is constructed by P60. -/
199 theorem population_atlas_law (T S : Operator r)
200     (C : A → Fin (degree+1) → Operator r)
201     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
202     {q bound : ℕ}
203     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J (fittedCoefficients T S C) q bound)
204     (U : State r ≃ₗ[ℝ] State r) (π : ContinuousRecords.Policy (A := A) (Y := ℝ))
205     (z₀ : State r) (N : ℕ) :
206     ContinuousRecords.recordLaw
207       (CertifiedTemplate.fittedInstrument M b (fittedCoefficients T S C)
208         (atlasCoefficients U (fittedCoefficients T S C)) W U
209         (atlas_coefficient_match U (fittedCoefficients T S C))) π (U (T *ᵥ z₀)) N=
210       ContinuousRecords.recordLaw (realizedInstrument T S C M b W) π (T *ᵥ z₀) N :=
211   CertifiedTemplate.record_law_transport M b (fittedCoefficients T S C)
212     (atlasCoefficients U (fittedCoefficients T S C)) W U
213     (atlas_coefficient_match U (fittedCoefficients T S C)) π (T *ᵥ z₀) N
214 
215 end Atlas
216 
217 section CertifiedConsequences
218 variable (T S : Operator r) (C : A → Fin (degree+1) → Operator r)
219 variable (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
220 variable {q bound : ℕ}
221 variable (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J (fittedCoefficients T S C) q bound)
222 local notation "I₀" => realizedInstrument T S C M b W
223 
224 omit [MeasurableSingletonClass A] in
225 /-- Complete synthesis preserves the actual event measure. Signed component
226 packets are allowed here, without being assigned individual probability laws. -/
227 theorem complete_packet_law {K : Type*} [Fintype K]
228     (P : K → State r →ₗ[ℝ] State r) (hP : ∑ k,P k=LinearMap.id)
229     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (z₀ : State r) (N : ℕ) :
230     ContinuousRecords.recordLaw I₀ π (∑ k,P k (T *ᵥ z₀)) N=
231       ContinuousRecords.recordLaw I₀ π (T *ᵥ z₀) N := by
232   have hs : ∑ k,P k (T *ᵥ z₀)=T *ᵥ z₀ := by
233     simpa only [LinearMap.sum_apply,LinearMap.id_apply] using
234       congrArg (fun L : State r →ₗ[ℝ] State r => L (T *ᵥ z₀)) hP
235   rw [hs]
236 
237 omit [DecidableEq D] in
238 /-- Individual normalized packets require their own positivity and positive
239 mass. The complete synthesis identity alone is not used as a positivity proof. -/
240 theorem positive_packet_state (P : State r →ₗ[ℝ] State r)
241     (hpositive : ∀ x∈M.cone,P x∈M.cone) (z₀ : State r)
242     (hinitial : (M.J (T *ᵥ z₀)).PosSemidef ∧ M.mass (T *ᵥ z₀)=1)
243     (hmass : 0<M.mass (P (T *ᵥ z₀))) :
244     (M.mass (P (T *ᵥ z₀)))⁻¹ • P (T *ᵥ z₀)∈M.coneInstance.base :=
245   PositivePackets.normalized_packet M.coneInstance.carrier
246     (fun _ ha _ hx => M.coneInstance.smul_mem ha hx) M.mass P hpositive
247     (T *ᵥ z₀) hinitial.1 hmass
248 
249 /-- The exact finite event model is the literal bin pushforward under any
250 policy depending on the full action/bin history. The partition map is built
251 from the supplied measurable covering cells rather than assumed as a law. -/
252 theorem exact_population_bins {J : Type*} [MeasurableSpace J] [Fintype J]
253     [MeasurableSingletonClass J] (cells : J → Set ℝ)
254     (hcover : ⋃ j,cells j=Set.univ)
255     (hdisjoint : Pairwise (fun i j => Disjoint (cells i) (cells j)))
256     (hmeas : ∀ j,MeasurableSet (cells j))
257     (π : List (A × J) → A → ℝ) (hπ : ∀ h,FiniteBayes.IsPrior (π h))
258     (z₀ : State r) (hinitial : (M.J (T *ᵥ z₀)).PosSemidef ∧ M.mass (T *ᵥ z₀)=1) (N : ℕ) :
259     let bin := ContinuousBins.partitionBin cells hcover
260     (∀ j,bin ⁻¹' {j}=cells j) ∧
261     (ContinuousRecords.recordLaw I₀
262       (ContinuousBins.liftedBinPolicy bin
263         (ContinuousBins.partitionBin_measurable cells hcover hdisjoint hmeas) π hπ) (T *ᵥ z₀) N).map
264           (ContinuousBins.historyMap (ContinuousBins.binStep bin) N)=
265             ContinuousBins.finiteBinnedLaw I₀ bin π (T *ᵥ z₀) N := by
266   dsimp only
267   have hb : T *ᵥ z₀∈M.coneInstance.base := hinitial
268   have he := ContinuousBins.exact_partition_coarsening I₀ cells hcover hdisjoint hmeas π hπ
269     (T *ᵥ z₀) hb N
270   exact ⟨he.1,he.2.2.2⟩
271 
272 omit [MeasurableSpace A] [MeasurableSingletonClass A] in
273 /-- The positive cell approximation is built from this same fitted instrument
274 on the same cone/reference. Its averaging and resolution bound are derived. -/
275 theorem population_cell_resolution {J : Type*} [Fintype J]
276     (P : PositiveCellApproximation.CellPartition UniformIntervalMoments.measure J)
277     (L h : ℝ) (hL : 0≤L) (hh : 0≤h)
278     (hLip : PositiveCellApproximation.CellLipschitz I₀ P L)
279     (hDiameter : PositiveCellApproximation.CellDiameter P h) :
280     let K := PositiveCellApproximation.instrument I₀ P
281     (∀ a y x,x∈M.cone → K.op a y x∈M.cone) ∧
282     (∀ a x,M.mass ((∫ y,K.op a y∂UniformIntervalMoments.measure) x)=M.mass x) ∧
283     (∀ a j,ContinuousBins.cellOperator UniformIntervalMoments.measure (K.op a) (P.cell j)=
284       ContinuousBins.cellOperator UniformIntervalMoments.measure ((I₀).op a) (P.cell j)) ∧
285     (∀ a,IsMarkovKernel (K.kernel a)) ∧ PositiveCellApproximation.approximationError I₀ P≤L*h :=
286   PositiveCellApproximation.positive_cell_average_certificate I₀ P L h hL hh hLip hDiameter
287 
288 omit [MeasurableSpace A] [MeasurableSingletonClass A] in
289 /-- The sharper uniform-interval estimate also concerns the very same actual
290 fitted density, with its genuine induced base norm and actual interval cells. -/
291 theorem population_equal_interval_resolution {J : Type*} [Fintype J]
292     (P : PositiveCellApproximation.CellPartition UniformIntervalMoments.measure J)
293     (left right : J → ℝ) (L h : ℝ) (hL : 0≤L) (hh : 0<h)
294     (hcells : ∀ j,P.cell j=Set.Ioc (left j) (right j))
295     (hleft : ∀ j,-1≤left j) (hright : ∀ j,right j≤1) (hwidth : ∀ j,right j-left j=h)
296     (hLip : ∀ a,∀ y∈Set.Icc (-1 : ℝ) 1,∀ v∈Set.Icc (-1 : ℝ) 1,
297       PositiveCellApproximation.inducedNorm (C := M.coneInstance) ((I₀).op a y-(I₀).op a v)≤L*dist y v) :
298     PositiveCellApproximation.approximationError I₀ P≤L*h/3 :=
299   (PositiveCellApproximation.positive_equal_interval_certificate I₀ P left right L h hL hh
300     hcells hleft hright hwidth hLip).2.2.2.2
301 
302 end CertifiedConsequences
303 
304 section CommonPolicyBudget
305 
306 omit [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A] in
307 /-- The time-indexed law construction has the same chronological states when
308 the actual density instrument is stationary. -/
309 theorem stationary_run (C₀ : BaseNorm.ProbabilityCone (State r))
310     (J : ContinuousInstrument.DensityInstrument (A := A) C₀ UniformIntervalMoments.measure)
311     (x : State r) : (N : ℕ) → ∀ h : ContinuousRecords.History (A × ℝ) N,
312       TimeRecords.run (fun _ => J) x N h=ContinuousRecords.run J x N h
313   | 0,_ => rfl
314   | N+1,h => by
315     change J.op h.2.1 h.2.2 (TimeRecords.run (fun _ => J) x N h.1)=_
316     rw [stationary_run C₀ J x N h.1]
317     rfl
318 
319 omit [MeasurableSingletonClass A] in
320 /-- Equality is proved for the actual measures, so a P59 bound for the constant
321 time family is a bound for the same stationary fitted record law. -/
322 theorem stationary_record_law (C₀ : BaseNorm.ProbabilityCone (State r))
323     (J : ContinuousInstrument.DensityInstrument (A := A) C₀ UniformIntervalMoments.measure)
324     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (x : State r) (N : ℕ) :
325     TimeRecords.recordLaw (fun _ => J) π x N=ContinuousRecords.recordLaw J π x N := by
326   unfold TimeRecords.recordLaw ContinuousRecords.recordLaw
327   congr 1
328   funext h
329   simp only [TimeRecords.recordDensity,ContinuousRecords.recordDensity,stationary_run]
330 
331 /-- The actual reconstructed/certified law is compared only with certified
332 models on the same cone and reference, using one common history policy.
333 The instrument and initial discrepancies remain explicit source hypotheses. -/
334 theorem population_common_policy_budget (T S : Operator r)
335     (C : A → Fin (degree+1) → Operator r)
336     (M : MatrixEmbedding.Embedding (State r) D) (b : Module.Basis R ℝ (State r))
337     {q bound : ℕ}
338     (W : PolynomialGram.CoefficientCertificate b M.coneInstance M.J (fittedCoefficients T S C) q bound)
339     (others : ℕ → ContinuousInstrument.DensityInstrument (A := A) M.coneInstance UniformIntervalMoments.measure)
340     (π : ContinuousRecords.Policy (A := A) (Y := ℝ))
341     (z₀ : State r) (hinitial : T *ᵥ z₀∈M.coneInstance.base)
342     (otherInitial : ContinuousInstrument.DensityInstrument.State M.coneInstance)
343     (ε : ℕ → ℝ) (hε : ∀ t,0≤ε t)
344     (herror : ∀ t a x,x∈M.coneInstance.base →
345       (∫ y,M.coneInstance.value
346         ((realizedInstrument T S C M b W).op a y x-(others t).op a y x)
347           ∂UniformIntervalMoments.measure)≤ε t)
348     (e₀ : ℝ) (hinitialError : M.coneInstance.value (T *ᵥ z₀-otherInitial.1)≤e₀) (N : ℕ) :
349     let initial : ContinuousInstrument.DensityInstrument.State M.coneInstance := ⟨T *ᵥ z₀,hinitial⟩
350     letI : IsProbabilityMeasure (TimeRecords.recordLaw (fun _ => realizedInstrument T S C M b W) π initial.1 N) :=
351       TimeRecords.recordLaw_probability (fun _ => realizedInstrument T S C M b W) π initial N
352     letI : IsProbabilityMeasure (TimeRecords.recordLaw others π otherInitial.1 N) :=
353       TimeRecords.recordLaw_probability others π otherInitial N
354     TimeRecords.recordLaw (fun _ => realizedInstrument T S C M b W) π initial.1 N=
355       ContinuousRecords.recordLaw (realizedInstrument T S C M b W) π initial.1 N ∧
356     SequentialLowerCertificate.lawTV
357       (TimeRecords.recordLaw (fun _ => realizedInstrument T S C M b W) π initial.1 N)
358       (TimeRecords.recordLaw others π otherInitial.1 N)≤min 1 ((e₀+∑ t∈Finset.range N,ε t)/2) := by
359   dsimp only
360   exact ⟨stationary_record_law M.coneInstance (realizedInstrument T S C M b W) π (T *ᵥ z₀) N,
361     ContinuousTV.record_lawTV_le (fun _ => realizedInstrument T S C M b W) others π
362       ⟨T *ᵥ z₀,hinitial⟩ otherInitial ε hε herror e₀ hinitialError N⟩
363 
364 end CommonPolicyBudget
365 
366 end Komorebi.LSM.ContinuousRealizationP61

Back to source controls