DecisionHistory.lean

1 import MachineTheory.ResponseDecision
2 
3 /-!
4 A checked bridge from Block04's actual history laws to Core4.1. Conditioning,
5 projection, record rounding and response approximation all refer to one event
6 and the same candidate coordinates. Conditional certificates require positive
7 mass under both laws; external access to the conditioning event is not inferred.
8 -/
9 namespace Komorebi.MachineTheory.DecisionHistory
10 open scoped BigOperators
11 open Instrument Variation ApproximateHistory ApproximateDecision ResponseDecision
12 noncomputable section
13 universe u
14 variable {X Y I V : Type*}
15 
16 /-- Retain the requested coordinate only after conditioning on the named event. -/
17 def recordAfter [Fintype X] [DecidableEq X] [DecidableEq Y]
18     (f : X → Y) (E : Finset X) (p : X → ℝ) : Y → ℝ :=
19   push f (normalize (restrict E p))
20 
21 theorem recordAfter_dist [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
22     (f : X → Y) (E : Finset X) (p : X → ℝ) (hp : IsDist p)
23     (hE : 0 < mass (restrict E p)) : IsDist (recordAfter f E p) :=
24   push_dist f _ (normalize_dist _ (restrict_nonneg E p hp.1) hE)
25 
26 /-- The record error includes conditioning and any further storage perturbation. -/
27 def recordAllowance [Fintype X] [DecidableEq X]
28     (E : Finset X) (p q : X → ℝ) (δ s : ℝ) : ℝ :=
29   min 1 (min 1 (δ / max (mass (restrict E p)) (mass (restrict E q))) + s)
30 
31 theorem conditioning_and_storage [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
32     (f : X → Y) (E : Finset X) (p q : X → ℝ) (r : Y → ℝ)
33     (hp : IsDist p) (hq : IsDist q) (hr : IsDist r)
34     (hEp : 0 < mass (restrict E p)) (hEq : 0 < mass (restrict E q))
35     (δ s : ℝ) (hδ : tv p q ≤ δ) (hs : tv (recordAfter f E q) r ≤ s) :
36     tv (recordAfter f E p) r ≤ recordAllowance E p q δ s := by
37   apply le_min
38   · exact tv_le_one _ _ (recordAfter_dist f E p hp hEp) hr
39   · have h := conditional_output_bound f E p q hp hq hEp hEq δ hδ
40     exact (tv_triangle (recordAfter f E p) (recordAfter f E q) r).trans (add_le_add h hs)
41 
42 /-- The complete record/response inequality after an actual event and stored-record revision. -/
43 theorem conditioned_response_error [Fintype X] [Fintype Y]
44     [DecidableEq X] [DecidableEq Y] [PseudoMetricSpace V]
45     (f : X → Y) (E : Finset X) (p q : X → ℝ) (r : Y → ℝ)
46     (hp : IsDist p) (hq : IsDist q) (hr : IsDist r)
47     (hEp : 0 < mass (restrict E p)) (hEq : 0 < mass (restrict E q))
48     (δ s : ℝ) (hδ : tv p q ≤ δ) (hs : tv (recordAfter f E q) r ≤ s)
49     (v w : Y → V) (loss : I → V → ℝ) (i : I) (K d : ℝ) (hK : 0 ≤ K)
50     (hd : ∀ y, dist (v y) (w y) ≤ d)
51     (hlip : ∀ y, |loss i (v y)-loss i (w y)| ≤ K*dist (v y) (w y))
52     (hv : ∀ y, 0 ≤ loss i (v y) ∧ loss i (v y) ≤ 1)
53     (hw : ∀ y, 0 ≤ loss i (w y) ∧ loss i (w y) ≤ 1) :
54     |responseRisk (recordAfter f E p) v loss i-responseRisk r w loss i| ≤
55       allowance (recordAllowance E p q δ s) K d :=
56   decision_error _ r v w loss i (recordAfter_dist f E p hp hEp) hr _ K d hK
57     (conditioning_and_storage f E p q r hp hq hr hEp hEq δ s hδ hs) hd hlip hv hw
58 
59 /-- Report/next-state law generated by an instrument and a prior. -/
60 def jointKernel {S A O : Type u} [Fintype S] [Fintype O] (K : Law S A O) (a : A) :
61     Kernel S (O × S) where
62   entry y x := jointRow K a x y
63   nonnegative y x := (jointRow_dist K a x).1 y
64   normalized x := (jointRow_dist K a x).2
65 
66 def jointEvidence {S A O : Type u} [Fintype S] [Fintype O]
67     (K : Law S A O) (a : A) (p : S → ℝ) : O × S → ℝ :=
68   applyKernel (jointKernel K a).entry p
69 
70 theorem jointEvidence_dist {S A O : Type u} [Fintype S] [Fintype O]
71     (K : Law S A O) (a : A) (p : S → ℝ) (hp : IsDist p) :
72     IsDist (jointEvidence K a p) := kernel_dist (jointKernel K a) p hp
73 
74 /-- The model discrepancy is obtained from complete instrument rows, not scalar accuracy alone. -/
75 theorem jointEvidence_error {S Z A O : Type u}
76     [Fintype S] [Fintype Z] [Fintype O] [DecidableEq Z] [DecidableEq O]
77     (π : S → Z) (K : Law S A O) (L : Law Z A O) (a : A)
78     (p : S → ℝ) (q : Z → ℝ) (hp : IsDist p) (δ ε : ℝ)
79     (h0 : tv (push π p) q ≤ δ)
80     (hε : ∀ x, tv (push (reportMap π) (jointRow K a x)) (jointRow L a (π x)) ≤ ε) :
81     tv (push (reportMap π) (jointEvidence K a p)) (jointEvidence L a q) ≤ δ+ε :=
82   (push_kernel_step π (reportMap π) (jointKernel K a) (jointKernel L a)
83     p q hp ε hε).trans (add_le_add h0 (le_refl ε))
84 
85 variable {S Z A O : Type u}
86 
87 /-- The full-history result and response estimate are composed on the same realized laws. -/
88 theorem history_response_error [Fintype S] [Fintype Z] [Fintype A] [Fintype O]
89     [DecidableEq S] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
90     [Fintype Y] [DecidableEq Y] [PseudoMetricSpace V]
91     (π : S → Z) (K : Nat → Law S A O) (L : Nat → Law Z A O)
92     (g : Policy A O) (p : S → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
93     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
94     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
95     (H : Nat) (f : Path Z A O H → Y) (v w : Y → V) (loss : I → V → ℝ) (i : I)
96     (C d : ℝ) (hC : 0 ≤ C) (hd : ∀ y, dist (v y) (w y) ≤ d)
97     (hlip : ∀ y, |loss i (v y)-loss i (w y)| ≤ C*dist (v y) (w y))
98     (hv : ∀ y, 0 ≤ loss i (v y) ∧ loss i (v y) ≤ 1)
99     (hw : ∀ y, 0 ≤ loss i (w y) ∧ loss i (w y) ≤ 1) :
100     |responseRisk (push f (push (project π H) (law K g p H))) v loss i-
101       responseRisk (push f (law L g q H)) w loss i| ≤
102       allowance (min 1 (δ + ∑ n ∈ Finset.range H, ε n)) C d :=
103   decision_error _ _ v w loss i
104     (push_dist _ _ (push_dist _ _ (law_dist K g p hp H)))
105     (push_dist _ _ (law_dist L g q hq H)) _ C d hC
106     (observed_history_bound π K L g p q hp hq δ ε h0 hε H f) hd hlip hv hw
107 
108 /-- A complete event-conditioned history, followed by rounded storage and response approximation. -/
109 theorem history_conditioned_response_error [Fintype S] [Fintype Z] [Fintype A] [Fintype O]
110     [DecidableEq S] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
111     [Fintype Y] [DecidableEq Y] [PseudoMetricSpace V]
112     (π : S → Z) (K : Nat → Law S A O) (L : Nat → Law Z A O)
113     (g : Policy A O) (p : S → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
114     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
115     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
116     (H : Nat) (f : Path Z A O H → Y) (E : Finset (Path Z A O H))
117     (hEp : 0 < mass (restrict E (push (project π H) (law K g p H))))
118     (hEq : 0 < mass (restrict E (law L g q H)))
119     (r : Y → ℝ) (hr : IsDist r) (s : ℝ)
120     (hs : tv (recordAfter f E (law L g q H)) r ≤ s)
121     (v w : Y → V) (loss : I → V → ℝ) (i : I)
122     (C d : ℝ) (hC : 0 ≤ C) (hd : ∀ y, dist (v y) (w y) ≤ d)
123     (hlip : ∀ y, |loss i (v y)-loss i (w y)| ≤ C*dist (v y) (w y))
124     (hv : ∀ y, 0 ≤ loss i (v y) ∧ loss i (v y) ≤ 1)
125     (hw : ∀ y, 0 ≤ loss i (w y) ∧ loss i (w y) ≤ 1) :
126     |responseRisk (recordAfter f E (push (project π H) (law K g p H))) v loss i-
127       responseRisk r w loss i| ≤
128       allowance (recordAllowance E (push (project π H) (law K g p H))
129         (law L g q H) (min 1 (δ + ∑ n ∈ Finset.range H, ε n)) s) C d :=
130   conditioned_response_error f E _ _ r
131     (push_dist _ _ (law_dist K g p hp H)) (law_dist L g q hq H) hr hEp hEq
132     _ s (whole_history_bound π K L g p q hp hq δ ε h0 hε H) hs
133     v w loss i C d hC hd hlip hv hw
134 
135 end
136 end Komorebi.MachineTheory.DecisionHistory

Back to source controls