PolynomialGramP53.lean

1 import KomorebiLSM.PolynomialGram
2 import KomorebiLSM.MatrixEmbedding
3 import KomorebiLSM.ContinuousRecords
4 
5 /-! The full P53 endpoint combines the actual P50 embedded PSD domain, finite
6 polynomial coefficient/Gram data, actual uniform moments, and the P52 finite
7 record probability semantics. No stochastic validity is a certificate field. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.PolynomialGramP53
10 open PolynomialGram MeasureTheory ProbabilityTheory
11 
12 variable {E D A R : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
13 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
14 variable [Fintype D] [DecidableEq D] [Fintype A] [Fintype R]
15 variable [MeasurableSpace A] [MeasurableSingletonClass A]
16 variable (M : MatrixEmbedding.Embedding E D) (b : Module.Basis R ℝ E)
17 variable {n q bound : ℕ} (B : A → Fin n → E →L[ℝ] E)
18 variable (W : CoefficientCertificate b M.coneInstance M.J B q bound)
19 
20 /-- The finite witness constructs the literal polynomial density instrument
21 on the embedded matrix cone, not an abstract positive replacement. -/
22 noncomputable def instrument : ContinuousInstrument.DensityInstrument
23     (A := A) M.coneInstance UniformIntervalMoments.measure :=
24   W.instrument M.coneInstance_mem
25 
26 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [MeasurableSingletonClass A] in
27 @[simp] theorem instrument_op (a : A) (u : ℝ) :
28     (instrument M b B W).op a u=operatorPolynomial (B a) u := rfl
29 
30 /-- P53 for every observation value and every finite horizon. The true PSD
31 embedding/interior data are in `M`; the literal finite Gram, coefficient and
32 moment checks are in `W`. Initial positivity and normalization remain explicit. -/
33 theorem polynomial_gram_probability_certificate (z₀ : E)
34     (hz₀ : z₀∈M.cone ∧ M.mass z₀=1) :
35     let I := instrument M b B W
36     (∀ a u, u∈Set.Icc (-1 : ℝ) 1 → ∀ z∈M.cone,
37       operatorPolynomial (B a) u z∈M.cone) ∧
38     (∀ word : List (A × ℝ), (∀ s∈word,s.2∈Set.Icc (-1 : ℝ) 1) →
39       0≤M.mass (FiniteInstruments.wordAction
40         (fun s : A × ℝ => (operatorPolynomial (B s.1) s.2).toLinearMap) word z₀)) ∧
41     (∀ a u, u∈Set.Icc (-1 : ℝ) 1 → ∀ z∈M.coneInstance.base,
42       0<M.mass (operatorPolynomial (B a) u z) →
43       (M.mass (operatorPolynomial (B a) u z))⁻¹ • operatorPolynomial (B a) u z∈M.coneInstance.base) ∧
44     (∀ a, IsMarkovKernel (I.kernel a)) ∧
45     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ), ∀ T,
46       IsProbabilityMeasure (ContinuousRecords.recordLaw I π z₀ T)) ∧
47     (∀ π : ContinuousRecords.Policy (A := A) (Y := ℝ), ∀ T,
48       (ContinuousRecords.recordLaw I π z₀ (T+1)).fst=ContinuousRecords.recordLaw I π z₀ T) ∧
49     (∀ actions : ℕ → A, ∀ T,
50       IsProbabilityMeasure (ContinuousRecords.observationLaw I actions z₀ T)) ∧
51     (∀ actions : ℕ → A, ∀ T,
52       (ContinuousRecords.observationLaw I actions z₀ (T+1)).fst=
53         ContinuousRecords.observationLaw I actions z₀ T) ∧
54     (∀ actions : ℕ → A, ∀ T (S : Set (ContinuousRecords.History ℝ T)), MeasurableSet S →
55       ContinuousRecords.observationLaw I actions z₀ T S=
56         ∫⁻ h in S, ENNReal.ofReal (M.mass (ContinuousRecords.observationRun I actions z₀ T h))
57           ∂ContinuousRecords.reference UniformIntervalMoments.measure T) := by
58   dsimp only
59   have hbase : z₀∈M.coneInstance.base := hz₀
60   refine ⟨?_,?_,?_,?_,?_,?_,?_,?_,?_⟩
61   · intro a u hu z hz
62     exact W.positive a u hu z hz
63   · intro word hword
64     exact W.word_mass_nonnegative M.coneInstance_mem word hword z₀ hz₀.1
65   · intro a u hu z hz hp
66     exact W.normalized_update M.coneInstance_mem a u hu z hz hp
67   · intro a
68     infer_instance
69   · intro π T
70     exact ContinuousRecords.recordLaw_probability (instrument M b B W) π ⟨z₀,hbase⟩ T
71   · intro π T
72     exact ContinuousRecords.recordLaw_consistent (instrument M b B W) π hbase.1 T
73   · intro actions T
74     exact ContinuousRecords.observationLaw_probability (instrument M b B W) actions ⟨z₀,hbase⟩ T
75   · intro actions T
76     exact ContinuousRecords.observationLaw_consistent (instrument M b B W) actions hbase.1 T
77   · intro actions T S hS
78     exact ContinuousRecords.observationLaw_product_density (instrument M b B W) actions z₀ T S hS
79 
80 end Komorebi.LSM.PolynomialGramP53

Back to source controls