StructuredRectangle.lean

1 import KomorebiLSM.CurvedMomentRecordTV
2 import KomorebiLSM.MarkovWindows
3 
4 /-! P87's deterministic whole-rectangle certificate. The returned instruments,
5 observation records, Markov marginals and rolling windows are the actual laws
6 of the declared curved-moment family. Statistical coverage is a separate input
7 to the consuming process theorem, never an assumption of these domain bounds. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.CurvedMoment.StructuredRectangle
10 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MarkovStability
11 open scoped ENNReal
12 noncomputable section
13 
14 structure Rectangle where
15   lowerA : ℝ
16   upperA : ℝ
17   lowerB : ℝ
18   upperB : ℝ
19 
20 namespace Rectangle
21 
22 def carrier (B : Rectangle) : Set (ℝ × ℝ) :=
23   {q | q.1∈Set.Icc B.lowerA B.upperA ∧ q.2∈Set.Icc B.lowerB B.upperB}
24 
25 def boundA (B : Rectangle) : ℝ := max |B.lowerA| |B.upperA|
26 def boundB (B : Rectangle) : ℝ := max |B.lowerB| |B.upperB|
27 def densityFloor (B : Rectangle) : ℝ := 1-B.boundA-B.boundB
28 def distanceA (B : Rectangle) (center : ℝ × ℝ) : ℝ :=
29   max |B.lowerA-center.1| |B.upperA-center.1|
30 def distanceB (B : Rectangle) (center : ℝ × ℝ) : ℝ :=
31   max |B.lowerB-center.2| |B.upperB-center.2|
32 
33 theorem interval_abs_le (l u a : ℝ) (ha : a∈Set.Icc l u) :
34     |a|≤max |l| |u| := by
35   apply abs_le.mpr
36   constructor
37   · exact (neg_le_neg (le_max_left |l| |u|)).trans ((neg_abs_le l).trans ha.1)
38   · exact ha.2.trans ((le_abs_self u).trans (le_max_right |l| |u|))
39 
40 theorem interval_distance_le (l u c a : ℝ) (ha : a∈Set.Icc l u) :
41     |a-c|≤max |l-c| |u-c| :=
42   interval_abs_le (l-c) (u-c) (a-c) ⟨sub_le_sub_right ha.1 c,sub_le_sub_right ha.2 c⟩
43 
44 theorem member_diamond (B : Rectangle) {q : ℝ × ℝ} (hq : q∈B.carrier) :
45     |q.1|+|q.2|≤1-B.densityFloor := by
46   have ha := interval_abs_le B.lowerA B.upperA q.1 hq.1
47   have hb := interval_abs_le B.lowerB B.upperB q.2 hq.2
48   change |q.1|+|q.2|≤1-(1-max |B.lowerA| |B.upperA|-max |B.lowerB| |B.upperB|)
49   linarith
50 
51 theorem densityFloor_le_one (B : Rectangle) : B.densityFloor≤1 := by
52   have ha : 0≤B.boundA := (abs_nonneg B.lowerA).trans (le_max_left _ _)
53   have hb : 0≤B.boundB := (abs_nonneg B.lowerB).trans (le_max_left _ _)
54   dsimp [densityFloor]
55   linarith
56 
57 theorem member_distances (B : Rectangle) (center : ℝ × ℝ) {q : ℝ × ℝ}
58     (hq : q∈B.carrier) :
59     |q.1-center.1|≤B.distanceA center ∧ |q.2-center.2|≤B.distanceB center :=
60   ⟨interval_distance_le _ _ _ _ hq.1,interval_distance_le _ _ _ _ hq.2⟩
61 
62 theorem distanceA_nonneg (B : Rectangle) (center : ℝ × ℝ) : 0≤B.distanceA center :=
63   (abs_nonneg _).trans (le_max_left _ _)
64 theorem distanceB_nonneg (B : Rectangle) (center : ℝ × ℝ) : 0≤B.distanceB center :=
65   (abs_nonneg _).trans (le_max_left _ _)
66 
67 variable {μ : Measure ℝ} (R : Reference μ)
68 
69 /-- Every member, including the endpoints, defines its literal positive,
70 integrated-mass-preserving operator on the full curved cone. -/
71 def instrument (B : Rectangle) (hfloor : 0≤B.densityFloor) (q : ℝ × ℝ)
72     (hq : q∈B.carrier) :
73     ContinuousInstrument.DensityInstrument (A:=Unit) probabilityCone μ :=
74   R.instrument q.1 q.2 B.densityFloor hfloor (B.member_diamond hq)
75 
76 /-- Every finite horizon is a probability law; the geometry certificate
77 covers the entire rectangle rather than only its selected center. -/
78 theorem all_horizon_probability (B : Rectangle) (hfloor : 0≤B.densityFloor)
79     (q : ℝ × ℝ) (hq : q∈B.carrier)
80     (π : ContinuousRecords.Policy (A:=Unit) (Y:=ℝ))
81     (z : ContinuousInstrument.DensityInstrument.State probabilityCone) (n : ℕ) :
82     IsProbabilityMeasure (ContinuousRecords.recordLaw (B.instrument R hfloor q hq) π z.1 n) := by
83   let := R.probability
84   exact ContinuousRecords.recordLaw_probability _ π z n
85 
86 def kernel (B : Rectangle) (hfloor : 0≤B.densityFloor) (q : ℝ × ℝ)
87     (hq : q∈B.carrier) : Kernel ℝ ℝ :=
88   R.completedKernel q.1 q.2 B.densityFloor hfloor (B.member_diamond hq)
89 
90 instance kernel_markov (B : Rectangle) (hfloor : 0≤B.densityFloor) (q : ℝ × ℝ)
91     (hq : q∈B.carrier) : IsMarkovKernel (B.kernel R hfloor q hq) := by
92   unfold kernel
93   infer_instance
94 
95 def errorBudget (B : Rectangle) (center : ℝ × ℝ) : ℝ :=
96   R.parameterBudget (B.distanceA center) (B.distanceB center)
97 
98 theorem errorBudget_nonneg (B : Rectangle) (center : ℝ × ℝ) : 0≤B.errorBudget R center :=
99   R.parameterBudget_nonneg (B.distanceA_nonneg center) (B.distanceB_nonneg center)
100 
101 instance instrument_observation_probability (B : Rectangle) (hfloor : 0≤B.densityFloor)
102     (q : ℝ × ℝ) (hq : q∈B.carrier) (s : Signal) (T : ℕ) : IsProbabilityMeasure
103       (ContinuousRecords.observationLaw (B.instrument R hfloor q hq) (fun _ => ()) (curve s) T) := by
104   unfold instrument
105   infer_instance
106 
107 /-- Exact next-observation TV for every common normalized state. -/
108 theorem observation_bound [IsProbabilityMeasure μ] (B : Rectangle) (hfloor : 0≤B.densityFloor)
109     (q center : ℝ × ℝ) (hq : q∈B.carrier) (hc : center∈B.carrier)
110     (z : ContinuousInstrument.DensityInstrument.State probabilityCone) :
111     lawTV ((B.instrument R hfloor q hq).kernel () z)
112       ((B.instrument R hfloor center hc).kernel () z)≤B.errorBudget R center := by
113   obtain ⟨ha,hb⟩ := B.member_distances center hq
114   exact R.observation_lawTV_le q.1 q.2 B.densityFloor center.1 center.2 B.densityFloor
115     (B.distanceA center) (B.distanceB center) hfloor (B.member_diamond hq)
116     hfloor (B.member_diamond hc) ha hb z
117 
118 /-- Parameter uncertainty yields the actual operator-product record bound,
119 without adding a state-estimation term. -/
120 theorem complete_record_bound (B : Rectangle) (hfloor : 0≤B.densityFloor)
121     (q center : ℝ × ℝ) (hq : q∈B.carrier) (hc : center∈B.carrier)
122     (s : Signal) (T : ℕ) :
123     lawTV (ContinuousRecords.observationLaw (B.instrument R hfloor q hq)
124       (fun _ => ()) (curve s) T)
125       (ContinuousRecords.observationLaw (B.instrument R hfloor center hc)
126         (fun _ => ()) (curve s) T)≤min 1 ((T:ℝ)*B.errorBudget R center) := by
127   obtain ⟨ha,hb⟩ := B.member_distances center hq
128   exact R.observationLaw_lawTV_le q.1 q.2 B.densityFloor center.1 center.2 B.densityFloor
129     (B.distanceA center) (B.distanceB center) hfloor (B.member_diamond hq)
130     hfloor (B.member_diamond hc) ha hb s T
131 
132 /-- The completed autonomous kernels retain the same pointwise row budget,
133 including declared completions at histories outside the interval support. -/
134 theorem kernel_row_bound (B : Rectangle) (hfloor : 0≤B.densityFloor)
135     (q center : ℝ × ℝ) (hq : q∈B.carrier) (hc : center∈B.carrier) (u : ℝ) :
136     lawTV (B.kernel R hfloor q hq u) (B.kernel R hfloor center hc u)≤B.errorBudget R center := by
137   obtain ⟨ha,hb⟩ := B.member_distances center hq
138   exact R.signalKernel_lawTV_le q.1 q.2 B.densityFloor center.1 center.2 B.densityFloor
139     (B.distanceA center) (B.distanceB center) hfloor (B.member_diamond hq)
140     hfloor (B.member_diamond hc) ha hb (observedSignal u)
141 
142 /-- The density floor is an actual measure minorization, not an asserted
143 contraction coefficient. The same reference measure works for every member. -/
144 theorem kernel_minorized (B : Rectangle) (hfloor : 0≤B.densityFloor)
145     (q : ℝ × ℝ) (hq : q∈B.carrier) :
146     Minorized (B.kernel R hfloor q hq) B.densityFloor μ := by
147   intro u
148   change ENNReal.ofReal B.densityFloor • μ≤
149     R.signalKernel q.1 q.2 B.densityFloor hfloor (B.member_diamond hq) (observedSignal u)
150   rw [R.signalKernel_apply]
151   calc
152     ENNReal.ofReal B.densityFloor • μ=
153         μ.withDensity (fun _ => ENNReal.ofReal B.densityFloor) := by simp
154     _ ≤ _ := by
155       apply withDensity_mono
156       filter_upwards [R.support] with v hv
157       apply ENNReal.ofReal_le_ofReal
158       have hz : curve (observedSignal u)∈normalized := by
159         rw [←base_eq_normalized]
160         exact (curveState (observedSignal u)).2
161       have hl := likelihood_lower q.1 q.2 B.densityFloor v hfloor (B.member_diamond hq) hv hz
162       convert hl using 1
163       simp [likelihood,curve]
164       ring
165 
166 /-- The exact geometric marginal estimate for the actual autonomous kernels,
167 including the complete-refresh endpoint when the floor equals one. -/
168 theorem marginal_bound (B : Rectangle) (hfloor : 0≤B.densityFloor)
169     (hpositive : 0<B.densityFloor) (q center : ℝ × ℝ)
170     (hq : q∈B.carrier) (hc : center∈B.carrier)
171     (ν η : Measure ℝ) [IsProbabilityMeasure ν] [IsProbabilityMeasure η] (t : ℕ) :
172     lawTV (MarkovStability.marginal (B.kernel R hfloor q hq) ν t)
173       (MarkovStability.marginal (B.kernel R hfloor center hc) η t)≤
174       min 1 ((1-B.densityFloor)^t*lawTV ν η+
175         B.errorBudget R center*(1-(1-B.densityFloor)^t)/B.densityFloor) := by
176   let := R.probability
177   exact MarkovStability.marginal_bound _ _ μ _ _ hpositive B.densityFloor_le_one
178     (B.kernel_minorized R hfloor q hq) (B.kernel_row_bound R hfloor q center hq hc) ν η t
179 
180 /-- A common initial law gives the uniform all-time one-marginal bound. -/
181 theorem marginal_uniform (B : Rectangle) (hfloor : 0≤B.densityFloor)
182     (hpositive : 0<B.densityFloor) (q center : ℝ × ℝ)
183     (hq : q∈B.carrier) (hc : center∈B.carrier)
184     (ν : Measure ℝ) [IsProbabilityMeasure ν] (t : ℕ) :
185     lawTV (MarkovStability.marginal (B.kernel R hfloor q hq) ν t)
186       (MarkovStability.marginal (B.kernel R hfloor center hc) ν t)≤
187       min 1 (B.errorBudget R center/B.densityFloor) := by
188   let := R.probability
189   exact MarkovStability.marginal_same_initial_uniform _ _ μ _ _ hpositive B.densityFloor_le_one
190     (B.errorBudget_nonneg R center) (B.kernel_minorized R hfloor q hq)
191     (B.kernel_row_bound R hfloor q center hq hc) ν t
192 
193 /-- L transitions contain L+1 consecutive observations; the literal rolling
194 window has the geometric entry-state budget plus L conditional-law errors. -/
195 theorem rolling_window_bound (B : Rectangle) (hfloor : 0≤B.densityFloor)
196     (hpositive : 0<B.densityFloor) (q center : ℝ × ℝ)
197     (hq : q∈B.carrier) (hc : center∈B.carrier)
198     (ν η : Measure ℝ) [IsProbabilityMeasure ν] [IsProbabilityMeasure η] (t L : ℕ) :
199     lawTV (rollingWindowLaw (B.kernel R hfloor q hq) ν t L)
200       (rollingWindowLaw (B.kernel R hfloor center hc) η t L)≤
201       min 1 ((1-B.densityFloor)^t*lawTV ν η+
202         B.errorBudget R center*(1-(1-B.densityFloor)^t)/B.densityFloor+
203           (L:ℝ)*B.errorBudget R center) := by
204   let := R.probability
205   exact MarkovStability.rollingWindow_geometric_bound _ _ μ _ _ hpositive B.densityFloor_le_one
206     (B.kernel_minorized R hfloor q hq) (B.kernel_row_bound R hfloor q center hq hc) ν η t L
207 
208 /-- The common-initial-law window bound is uniform in its start time, while
209 still retaining one conditional-law error for each additional observation. -/
210 theorem rolling_window_uniform (B : Rectangle) (hfloor : 0≤B.densityFloor)
211     (hpositive : 0<B.densityFloor) (q center : ℝ × ℝ)
212     (hq : q∈B.carrier) (hc : center∈B.carrier)
213     (ν : Measure ℝ) [IsProbabilityMeasure ν] (t L : ℕ) :
214     lawTV (rollingWindowLaw (B.kernel R hfloor q hq) ν t L)
215       (rollingWindowLaw (B.kernel R hfloor center hc) ν t L)≤
216       min 1 (B.errorBudget R center/B.densityFloor+(L:ℝ)*B.errorBudget R center) := by
217   let := R.probability
218   exact MarkovStability.rollingWindow_same_initial_uniform _ _ μ _ _ hpositive B.densityFloor_le_one
219     (B.errorBudget_nonneg R center) (B.kernel_minorized R hfloor q hq)
220     (B.kernel_row_bound R hfloor q center hq hc) ν t L
221 
222 end Rectangle
223 end
224 end Komorebi.LSM.CurvedMoment.StructuredRectangle

Back to source controls