ApproximateHistory.lean

1 import MachineTheory.Variation
2 import MachineTheory.Feedback
3 
4 /-!
5 Core 3.8, whole-history approximation.
6 A path retains every hidden state for mathematical comparison. The policy sees only its
7 previous actions and reports. Projection retains every coarse state, not just the final one.
8 Instruments may vary with time, with a separate uniform joint-row defect at each step.
9 -/
10 namespace Komorebi.MachineTheory.ApproximateHistory
11 open scoped BigOperators
12 open Instrument Variation
13 noncomputable section
14 universe u
15 variable {X Z A O : Type u}
16 
17 /-- Chronological trace: initial state, followed by action/report/successor triples. -/
18 @[reducible] def Path (X A O : Type u) : Nat → Type u
19   | 0 => X
20   | n+1 => Path X A O n × (A × O × X)
21 
22 instance pathFintype [Fintype X] [Fintype A] [Fintype O] (n : Nat) : Fintype (Path X A O n) := by
23   induction n with
24   | zero => exact inferInstanceAs (Fintype X)
25   | succ n ih =>
26     letI := ih
27     exact inferInstanceAs (Fintype (Path X A O n × (A × O × X)))
28 
29 instance pathDecidableEq [DecidableEq X] [DecidableEq A] [DecidableEq O] (n : Nat) :
30     DecidableEq (Path X A O n) := by
31   induction n with
32   | zero => exact inferInstanceAs (DecidableEq X)
33   | succ n ih =>
34     letI := ih
35     exact inferInstanceAs (DecidableEq (Path X A O n × (A × O × X)))
36 
37 def last : (n : Nat) → Path X A O n → X
38   | 0, x => x
39   | _+1, h => h.2.2.2
40 
41 /-- No state coordinate is exposed to this history interface. -/
42 def observed : (n : Nat) → Path X A O n → History A O
43   | 0, _ => []
44   | n+1, h => observed n h.1 ++ [(h.2.1,h.2.2.1)]
45 
46 def reportMap (π : X → Z) (u : O × X) : O × Z := (u.1,π u.2)
47 
48 def stepMap (π : X → Z) (u : A × O × X) : A × O × Z := (u.1,reportMap π u.2)
49 
50 def project (π : X → Z) : (n : Nat) → Path X A O n → Path Z A O n
51   | 0, x => π x
52   | n+1, h => (project π n h.1,stepMap π h.2)
53 
54 theorem project_last (π : X → Z) (n : Nat) (h : Path X A O n) :
55     last n (project π n h) = π (last n h) := by
56   cases n <;> rfl
57 
58 theorem project_observed (π : X → Z) (n : Nat) (h : Path X A O n) :
59     observed n (project π n h) = observed n h := by
60   induction n with
61   | zero => rfl
62   | succ n ih => simp only [observed, project, stepMap, reportMap, ih]
63 
64 def jointRow [Fintype X] [Fintype O] (K : Law X A O) (a : A) (x : X) : O × X → ℝ :=
65   fun u => K.kernel a u.1 u.2 x
66 
67 theorem jointRow_dist [Fintype X] [Fintype O] (K : Law X A O) (a : A) (x : X) :
68     IsDist (jointRow K a x) := by
69   refine ⟨fun u => K.nonnegative a u.1 u.2 x, ?_⟩
70   simpa only [mass, jointRow, Fintype.sum_prod_type] using K.normalized a x
71 
72 def stepRow [Fintype X] [Fintype A] [Fintype O]
73     (K : Law X A O) (g : Policy A O) (past : History A O) (x : X) : A × O × X → ℝ :=
74   fun u => g.probability past u.1 * jointRow K u.1 x u.2
75 
76 theorem stepRow_dist [Fintype X] [Fintype A] [Fintype O]
77     (K : Law X A O) (g : Policy A O) (past : History A O) (x : X) :
78     IsDist (stepRow K g past x) := by
79   constructor
80   · intro u
81     exact mul_nonneg (g.nonnegative past u.1) (K.nonnegative u.1 u.2.1 u.2.2 x)
82   · simp only [mass, stepRow, jointRow, Fintype.sum_prod_type]
83     simp_rw [← Finset.mul_sum, K.normalized, mul_one]
84     exact g.normalized past
85 
86 /-- Append an observed step and its true successor to the complete path. -/
87 def pathKernel [Fintype X] [Fintype A] [Fintype O]
88     [DecidableEq X] [DecidableEq A] [DecidableEq O]
89     (K : Law X A O) (g : Policy A O) (n : Nat) : Kernel (Path X A O n) (Path X A O (n+1)) where
90   entry t h := push (fun u : A × O × X => (h,u)) (stepRow K g (observed n h) (last n h)) t
91   nonnegative t h := push_nonnegative _ _ (stepRow_dist K g (observed n h) (last n h)).1 t
92   normalized h := (mass_push _ _).trans (stepRow_dist K g (observed n h) (last n h)).2
93 
94 /-- The actual fine path law is evolved before any state coordinate is forgotten. -/
95 def law [Fintype X] [Fintype A] [Fintype O]
96     [DecidableEq X] [DecidableEq A] [DecidableEq O]
97     (K : Nat → Law X A O) (g : Policy A O) (p : X → ℝ) : (n : Nat) → Path X A O n → ℝ
98   | 0 => p
99   | n+1 => applyKernel (pathKernel (K n) g n).entry (law K g p n)
100 
101 @[simp] theorem law_zero [Fintype X] [Fintype A] [Fintype O]
102     [DecidableEq X] [DecidableEq A] [DecidableEq O]
103     (K : Nat → Law X A O) (g : Policy A O) (p : X → ℝ) : law K g p 0 = p := rfl
104 
105 theorem law_dist [Fintype X] [Fintype A] [Fintype O]
106     [DecidableEq X] [DecidableEq A] [DecidableEq O]
107     (K : Nat → Law X A O) (g : Policy A O) (p : X → ℝ) (hp : IsDist p) (n : Nat) :
108     IsDist (law K g p n) := by
109   induction n with
110   | zero => exact hp
111   | succ n ih => exact kernel_dist (pathKernel (K n) g n) _ ih
112 
113 /-- The path construction is the literal chronological product, not an assumed history law. -/
114 theorem law_succ [Fintype X] [Fintype A] [Fintype O]
115     [DecidableEq X] [DecidableEq A] [DecidableEq O]
116     (K : Nat → Law X A O) (g : Policy A O) (p : X → ℝ) (n : Nat)
117     (h : Path X A O n) (u : A × O × X) :
118     law K g p (n+1) (h,u) =
119       g.probability (observed n h) u.1 * (K n).kernel u.1 u.2.1 u.2.2 (last n h) * law K g p n h := by
120   simp [law, pathKernel, applyKernel, push, Prod.mk.injEq, ite_and, stepRow, jointRow]
121 
122 /-- Aggregation retains the complete report/successor association. -/
123 theorem push_stepRow [Fintype X] [Fintype A] [Fintype O]
124     [DecidableEq Z] [DecidableEq A] [DecidableEq O]
125     (π : X → Z) (K : Law X A O) (g : Policy A O) (past : History A O) (x : X) :
126     push (stepMap π) (stepRow K g past x) =
127       fun u => g.probability past u.1 * push (reportMap π) (jointRow K u.1 x) u.2 := by
128   funext u
129   rcases u with ⟨a,v⟩
130   change push (fun u : A × O × X => (u.1, reportMap π u.2))
131     (fun u => g.probability past u.1*jointRow K u.1 x u.2) (a,v) = _
132   rw [push_pair_right (reportMap π) (fun a v => g.probability past a * jointRow K a x v) a v]
133   change push (reportMap π) (scale (g.probability past a) (jointRow K a x)) v = _
134   rw [push_scale]
135   rfl
136 
137 /-- The policy has the same observed-history input and the same action probabilities. -/
138 theorem stepRow_error [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
139     [DecidableEq Z] [DecidableEq A] [DecidableEq O]
140     (π : X → Z) (K : Law X A O) (L : Law Z A O) (g : Policy A O)
141     (past : History A O) (x : X) (ε : ℝ)
142     (hε : ∀ a x, tv (push (reportMap π) (jointRow K a x)) (jointRow L a (π x)) ≤ ε) :
143     tv (push (stepMap π) (stepRow K g past x)) (stepRow L g past (π x)) ≤ ε := by
144   rw [push_stepRow]
145   exact tv_weighted_rows_le (g.probability past) ⟨g.nonnegative past,g.normalized past⟩
146     (fun a => push (reportMap π) (jointRow K a x)) (fun a => jointRow L a (π x)) ε (fun a => hε a x)
147 
148 /-- Appending the old path adds no error: it is the same recorded prefix on both sides. -/
149 theorem project_append [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
150     [DecidableEq X] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
151     (π : X → Z) (n : Nat) (h : Path X A O n) (p : A × O × X → ℝ) :
152     push (project π (n+1)) (push (fun u => (h,u)) p) =
153       push (fun u : A × O × Z => (project π n h,u)) (push (stepMap π) p) := by
154   rw [push_comp, push_comp]
155   rfl
156 
157 theorem pathKernel_error [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
158     [DecidableEq X] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
159     (π : X → Z) (K : Law X A O) (L : Law Z A O) (g : Policy A O)
160     (n : Nat) (ε : ℝ)
161     (hε : ∀ a x, tv (push (reportMap π) (jointRow K a x)) (jointRow L a (π x)) ≤ ε)
162     (h : Path X A O n) :
163     tv (push (project π (n+1)) (fun t => (pathKernel K g n).entry t h))
164       (fun t => (pathKernel L g n).entry t (project π n h)) ≤ ε := by
165   change tv (push (project π (n+1)) (push (fun u => (h,u)) _)) (push _ _) ≤ ε
166   rw [project_append]
167   simp only [project_observed, project_last]
168   exact (tv_push_le (fun u : A × O × Z => (project π n h,u)) _ _).trans
169     (stepRow_error π K L g (observed n h) (last n h) ε hε)
170 
171 /-- Core 3.8: accumulated error for the entire coarse-state and action/report path. -/
172 theorem whole_history_bound [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
173     [DecidableEq X] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
174     (π : X → Z) (K : Nat → Law X A O) (L : Nat → Law Z A O) (g : Policy A O)
175     (p : X → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
176     (δ : ℝ) (ε : Nat → ℝ)
177     (h0 : tv (push π p) q ≤ δ)
178     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
179     (H : Nat) :
180     tv (push (project π H) (law K g p H)) (law L g q H) ≤
181       min 1 (δ + ∑ n ∈ Finset.range H, ε n) := by
182   apply le_min
183   · exact tv_le_one _ _ (push_dist _ _ (law_dist K g p hp H)) (law_dist L g q hq H)
184   · induction H with
185     | zero =>
186       change tv (push π p) q ≤ δ + 0
187       simpa only [add_zero] using h0
188     | succ n ih =>
189       have hstep := push_kernel_step (project π n) (project π (n+1))
190         (pathKernel (K n) g n) (pathKernel (L n) g n)
191         (law K g p n) (law L g q n) (law_dist K g p hp n) (ε n)
192         (pathKernel_error π (K n) (L n) g n (ε n) (hε n))
193       change tv (push (project π (n+1)) (law K g p (n+1))) (law L g q (n+1)) ≤ _ at hstep
194       rw [Finset.sum_range_succ]
195       linarith
196 
197 /-- Any further observable projection inherits the full-history bound. -/
198 theorem observed_history_bound [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
199     [DecidableEq X] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
200     {Y : Type*} [Fintype Y] [DecidableEq Y]
201     (π : X → Z) (K : Nat → Law X A O) (L : Nat → Law Z A O) (g : Policy A O)
202     (p : X → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
203     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
204     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
205     (H : Nat) (f : Path Z A O H → Y) :
206     tv (push f (push (project π H) (law K g p H))) (push f (law L g q H)) ≤
207       min 1 (δ + ∑ n ∈ Finset.range H, ε n) :=
208   (tv_push_le f _ _).trans (whole_history_bound π K L g p q hp hq δ ε h0 hε H)
209 
210 /-- Core 3.8's posterior conclusion is derived from the same constructed full path laws. -/
211 theorem conditional_final_bound [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
212     [DecidableEq X] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
213     (π : X → Z) (K : Nat → Law X A O) (L : Nat → Law Z A O) (g : Policy A O)
214     (p : X → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
215     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
216     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
217     (H : Nat) (E : Finset (Path Z A O H))
218     (hEp : 0 < mass (restrict E (push (project π H) (law K g p H))))
219     (hEq : 0 < mass (restrict E (law L g q H))) :
220     tv (push (last H) (normalize (restrict E (push (project π H) (law K g p H)))))
221       (push (last H) (normalize (restrict E (law L g q H)))) ≤
222       min 1 ((min 1 (δ + ∑ n ∈ Finset.range H, ε n)) /
223         max (mass (restrict E (push (project π H) (law K g p H)))) (mass (restrict E (law L g q H)))) :=
224   conditional_output_bound (last H) E _ _ (push_dist _ _ (law_dist K g p hp H))
225     (law_dist L g q hq H) hEp hEq _ (whole_history_bound π K L g p q hp hq δ ε h0 hε H)
226 
227 /-- If either observed-event mass exceeds the common error budget, both posteriors are defined. -/
228 theorem history_event_positive [Fintype X] [Fintype Z] [Fintype A] [Fintype O]
229     [DecidableEq X] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
230     (π : X → Z) (K : Nat → Law X A O) (L : Nat → Law Z A O) (g : Policy A O)
231     (p : X → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
232     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
233     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
234     (H : Nat) (E : Finset (Path Z A O H))
235     (he : min 1 (δ + ∑ n ∈ Finset.range H, ε n) < mass (restrict E (push (project π H) (law K g p H))) ∨
236       min 1 (δ + ∑ n ∈ Finset.range H, ε n) < mass (restrict E (law L g q H))) :
237     0 < mass (restrict E (push (project π H) (law K g p H))) ∧
238     0 < mass (restrict E (law L g q H)) := by
239   have h := whole_history_bound π K L g p q hp hq δ ε h0 hε H
240   have hP := push_dist (project π H) _ (law_dist K g p hp H)
241   have hQ := law_dist L g q hq H
242   have hd := (tv_nonneg _ _).trans h
243   rcases he with hleft | hright
244   · exact ⟨hd.trans_lt hleft, event_positive E _ _ hP hQ _ h hleft⟩
245   · rw [tv_symm] at h
246     exact ⟨event_positive E _ _ hQ hP _ h hright, hd.trans_lt hright⟩
247 
248 end
249 end Komorebi.MachineTheory.ApproximateHistory

Back to source controls