StructuredLearningCapstone.lean

1 import KomorebiLSM.StructuredLearning
2 import KomorebiLSM.StructuredRectangle
3 
4 /-! Full P87: one all-time event covers the data-selected outward rectangle.
5 Every verified rectangle carries actual all-horizon probability laws and
6 parameter-to-law, complete-record, marginal and rolling-window bounds. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.CurvedMoment
9 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MarkovStability
10 noncomputable section
11 
12 namespace StructuredRectangle.Rectangle
13 variable {ν : Measure ℝ}
14 
15 /-- A derived theorem package for the entire submitted rectangle. Its fields
16 refer to actual measures and actual kernel iterates. No field is an assumption
17 in the construction below. -/
18 structure Certificate (B : StructuredRectangle.Rectangle) (R : Reference ν)
19     (hfloor : 0≤B.densityFloor) [IsProbabilityMeasure ν] : Prop where
20   probability : ∀ q (hq : q∈B.carrier)
21     (π : ContinuousRecords.Policy (A:=Unit) (Y:=ℝ))
22     (z : ContinuousInstrument.DensityInstrument.State probabilityCone) (n : ℕ),
23     IsProbabilityMeasure (ContinuousRecords.recordLaw (B.instrument R hfloor q hq) π z.1 n)
24   observation_error : ∀ q center (hq : q∈B.carrier) (hc : center∈B.carrier)
25     (z : ContinuousInstrument.DensityInstrument.State probabilityCone),
26     lawTV ((B.instrument R hfloor q hq).kernel () z)
27       ((B.instrument R hfloor center hc).kernel () z)≤B.errorBudget R center
28   record_error : ∀ q center (hq : q∈B.carrier) (hc : center∈B.carrier) (s : Signal) (T : ℕ),
29     lawTV (ContinuousRecords.observationLaw (B.instrument R hfloor q hq) (fun _ => ()) (curve s) T)
30       (ContinuousRecords.observationLaw (B.instrument R hfloor center hc) (fun _ => ()) (curve s) T)
31       ≤min 1 ((T:ℝ)*B.errorBudget R center)
32   marginal_geometric : ∀ (_hpositive : 0<B.densityFloor) q center
33     (hq : q∈B.carrier) (hc : center∈B.carrier) (η ζ : Measure ℝ)
34     [IsProbabilityMeasure η] [IsProbabilityMeasure ζ] (t : ℕ),
35     lawTV (marginal (B.kernel R hfloor q hq) η t)
36       (marginal (B.kernel R hfloor center hc) ζ t)≤
37       min 1 ((1-B.densityFloor)^t*lawTV η ζ+
38         B.errorBudget R center*(1-(1-B.densityFloor)^t)/B.densityFloor)
39   window_geometric : ∀ (_hpositive : 0<B.densityFloor) q center
40     (hq : q∈B.carrier) (hc : center∈B.carrier) (η ζ : Measure ℝ)
41     [IsProbabilityMeasure η] [IsProbabilityMeasure ζ] (t L : ℕ),
42     lawTV (rollingWindowLaw (B.kernel R hfloor q hq) η t L)
43       (rollingWindowLaw (B.kernel R hfloor center hc) ζ t L)≤
44       min 1 ((1-B.densityFloor)^t*lawTV η ζ+
45         B.errorBudget R center*(1-(1-B.densityFloor)^t)/B.densityFloor+
46           (L:ℝ)*B.errorBudget R center)
47   marginal_error : ∀ (_hpositive : 0<B.densityFloor) q center
48     (hq : q∈B.carrier) (hc : center∈B.carrier) (η : Measure ℝ) [IsProbabilityMeasure η] (t : ℕ),
49     lawTV (marginal (B.kernel R hfloor q hq) η t)
50       (marginal (B.kernel R hfloor center hc) η t)≤min 1 (B.errorBudget R center/B.densityFloor)
51   window_error : ∀ (_hpositive : 0<B.densityFloor) q center
52     (hq : q∈B.carrier) (hc : center∈B.carrier) (η : Measure ℝ) [IsProbabilityMeasure η] (t L : ℕ),
53     lawTV (rollingWindowLaw (B.kernel R hfloor q hq) η t L)
54       (rollingWindowLaw (B.kernel R hfloor center hc) η t L)
55       ≤min 1 (B.errorBudget R center/B.densityFloor+(L:ℝ)*B.errorBudget R center)
56 
57 /-- Deterministic internal validity is independent of whether a statistical
58 coverage event happens for a particular realized sample path. -/
59 theorem certificate (B : StructuredRectangle.Rectangle) (R : Reference ν)
60     (hfloor : 0≤B.densityFloor) : @Certificate ν B R hfloor R.probability := by
61   let := R.probability
62   exact ⟨B.all_horizon_probability R hfloor,B.observation_bound R hfloor,
63     B.complete_record_bound R hfloor,B.marginal_bound R hfloor,B.rolling_window_bound R hfloor,
64     B.marginal_uniform R hfloor,B.rolling_window_uniform R hfloor⟩
65 
66 end StructuredRectangle.Rectangle
67 
68 namespace Reference
69 variable {ν : Measure ℝ} {R : Reference ν} {a b : ℝ}
70 
71 /-- Whenever the true parameter belongs to a verified rectangle, its declared
72 actual law equals the certified member, rather than merely sharing moments. -/
73 theorem TrueKernel.matches_certified_member (K : R.TrueKernel a b)
74     (B : StructuredRectangle.Rectangle) (htrue : (a,b)∈B.carrier)
75     (hfloor : 0≤B.densityFloor) :
76     K.kernel=R.signalKernel a b B.densityFloor hfloor (B.member_diamond htrue) := by
77   ext s
78   rw [K.density,R.signalKernel_apply]
79 
80 namespace ObservableProcess
81 variable {Ω H : Type*} [mΩ : MeasurableSpace Ω] [mH : MeasurableSpace H]
82 variable {μ : Measure Ω} [IsProbabilityMeasure μ] {F : Filtration ℕ mΩ}
83 variable {K : R.TrueKernel a b} (P : R.ObservableProcess (H:=H) (μ:=μ) F K)
84 
85 def coverageEvent : Set Ω :=
86   RegressionConfidence.scalarGood 1 (1/40) P.designA P.responseA a∩
87     RegressionConfidence.scalarGood (3/4) (1/40) P.designB P.responseB b
88 
89 /-- The literal full outward-rounded rectangle from the two recorded scalar
90 regressions, with the prior intersection already included in its endpoints. -/
91 def returnedRectangle (endpointGrid n : ℕ) (ω : Ω) : StructuredRectangle.Rectangle where
92   lowerA := RationalRegressionConfidence.lower (10^12) endpointGrid 1 (1/40) P.designA P.responseA n ω
93   upperA := RationalRegressionConfidence.upper (10^12) endpointGrid 1 (1/40) P.designA P.responseA n ω
94   lowerB := RationalRegressionConfidence.lower (10^12) endpointGrid (3/4) (1/40) P.designB P.responseB n ω
95   upperB := RationalRegressionConfidence.upper (10^12) endpointGrid (3/4) (1/40) P.designB P.responseB n ω
96 
97 /-- Full conditional data-to-domain endpoint. The selected finite time may
98 depend arbitrarily on the same observed data because the original measurable
99 event already covers every finite time. Every center and candidate in the full
100 rectangle receives the deterministic certificate. No stopping theorem, sample
101 independence, hidden-state estimate or nominal-only geometry test is assumed. -/
102 theorem observable_structured_learning (endpointGrid : ℕ) (he : 0<endpointGrid)
103     (ha : |a|≤1) (hb : |b|≤1) :
104     MeasurableSet P.coverageEvent ∧ (19/20:ℝ)≤μ.real P.coverageEvent ∧
105     ∀ ω∈P.coverageEvent,∀ selectedTime : Ω → ℕ,
106       let B := P.returnedRectangle endpointGrid (selectedTime ω) ω
107       ∃ htrue : (a,b)∈B.carrier,∀ hfloor : 0≤B.densityFloor,
108         @StructuredRectangle.Rectangle.Certificate ν B R hfloor R.probability ∧
109         K.kernel=R.signalKernel a b B.densityFloor hfloor (B.member_diamond htrue) := by
110   obtain ⟨hG,hprob,hcoverage⟩ := P.simultaneous_rational_coverage endpointGrid he ha hb
111   refine ⟨hG,hprob,?_⟩
112   intro ω hω selectedTime
113   let B := P.returnedRectangle endpointGrid (selectedTime ω) ω
114   have htrue : (a,b)∈B.carrier := hcoverage ω hω (selectedTime ω)
115   refine ⟨htrue,fun hfloor => ⟨B.certificate R hfloor,?_⟩⟩
116   exact K.matches_certified_member B htrue hfloor
117 
118 end ObservableProcess
119 end Reference
120 end
121 end Komorebi.LSM.CurvedMoment

Back to source controls