ResponseDecision.lean

1 import MachineTheory.ApproximateDecision
2 import Mathlib.Topology.MetricSpace.Basic
3 
4 /-!
5 Core 4.1: one probability record and one paired response approximation support
6 one bounded decision. A change in the loss function, model set or evidence record
7 is not silently included in either allowance. All risks are exact model risks.
8 -/
9 namespace Komorebi.MachineTheory.ResponseDecision
10 open scoped BigOperators
11 open Instrument Variation ApproximateDecision
12 noncomputable section
13 variable {X I V : Type*}
14 
15 /-- The loss is evaluated at the actual response in each represented world. -/
16 def responseRisk [Fintype X] (p : X → ℝ) (v : X → V)
17     (loss : I → V → ℝ) (i : I) : ℝ := risk p (fun x => loss i (v x))
18 
19 /-- The exact expected loss discrepancy at a fixed probability record. -/
20 theorem loss_change_bound [Fintype X] (p f g : X → ℝ) (hp : ∀ x, 0 ≤ p x) :
21     |risk p f - risk p g| ≤ ∑ x, |f x-g x| * p x := by
22   calc
23     |risk p f-risk p g| = |∑ x, (f x-g x)*p x| := by
24       simp only [risk, Finset.sum_sub_distrib, sub_mul]
25     _ ≤ ∑ x, |(f x-g x)*p x| := Finset.abs_sum_le_sum_abs _ _
26     _ = _ := by simp only [abs_mul, abs_of_nonneg (hp _)]
27 
28 theorem loss_change_uniform [Fintype X] (p f g : X → ℝ) (hp : IsDist p)
29     (r : ℝ) (hr : ∀ x, |f x-g x| ≤ r) : |risk p f-risk p g| ≤ r := by
30   calc
31     _ ≤ ∑ x, |f x-g x| * p x := loss_change_bound p f g hp.1
32     _ ≤ ∑ x, r*p x := Finset.sum_le_sum
33       (fun x _ => mul_le_mul_of_nonneg_right (hr x) (hp.1 x))
34     _ = r := by rw [← Finset.mul_sum]; change r * mass p = r; rw [hp.2, mul_one]
35 
36 /-- Clipping a proved error allowance to the actual loss range does not weaken it. -/
37 def allowance (e K d : ℝ) : ℝ := min 1 (e+K*d)
38 
39 theorem allowance_nonneg (e K d : ℝ) (he : 0 ≤ e) (hK : 0 ≤ K) (hd : 0 ≤ d) :
40     0 ≤ allowance e K d := le_min (by norm_num) (add_nonneg he (mul_nonneg hK hd))
41 
42 theorem response_risk_range [Fintype X] (p : X → ℝ) (v : X → V)
43     (loss : I → V → ℝ) (i : I) (hp : IsDist p)
44     (hl : ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1) :
45     0 ≤ responseRisk p v loss i ∧ responseRisk p v loss i ≤ 1 :=
46   risk_range p _ hp 1 hl
47 
48 /-- The algebraic core allows a directly proved loss discrepancy without a metric. -/
49 theorem record_and_loss_error [Fintype X] (p q f g : X → ℝ)
50     (hp : IsDist p) (hq : IsDist q) (e r : ℝ)
51     (he : tv p q ≤ e) (hr : ∀ x, |f x-g x| ≤ r)
52     (hf : ∀ x, 0 ≤ f x ∧ f x ≤ 1) (hg : ∀ x, 0 ≤ g x ∧ g x ≤ 1) :
53     |risk p f-risk q g| ≤ min 1 (e+r) := by
54   apply le_min
55   · have h1 := risk_range p f hp 1 hf
56     have h2 := risk_range q g hq 1 hg
57     exact abs_le.mpr ⟨by linarith, by linarith⟩
58   · calc
59       _ ≤ |risk p f-risk p g| + |risk p g-risk q g| := abs_sub_le _ _ _
60       _ ≤ r + 1*e := add_le_add (loss_change_uniform p f g hp r hr)
61         (same_policy_error p q g hp hq 1 e (by norm_num) hg he)
62       _ = e+r := by ring
63 
64 /-- Core 4.1, uniform response form. Bounds on attained responses suffice. -/
65 theorem decision_error [Fintype X] [PseudoMetricSpace V]
66     (p q : X → ℝ) (v w : X → V) (loss : I → V → ℝ) (i : I)
67     (hp : IsDist p) (hq : IsDist q) (e K d : ℝ) (hK : 0 ≤ K)
68     (he : tv p q ≤ e) (hd : ∀ x, dist (v x) (w x) ≤ d)
69     (hlip : ∀ x, |loss i (v x)-loss i (w x)| ≤ K*dist (v x) (w x))
70     (hv : ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
71     (hw : ∀ x, 0 ≤ loss i (w x) ∧ loss i (w x) ≤ 1) :
72     |responseRisk p v loss i-responseRisk q w loss i| ≤ allowance e K d := by
73   exact record_and_loss_error p q _ _ hp hq e (K*d) he
74     (fun x => (hlip x).trans (mul_le_mul_of_nonneg_left (hd x) hK)) hv hw
75 
76 /-- Global bounded Lipschitz losses specialize to the exact source theorem. -/
77 theorem decision_error_global [Fintype X] [PseudoMetricSpace V]
78     (p q : X → ℝ) (v w : X → V) (loss : I → V → ℝ)
79     (hp : IsDist p) (hq : IsDist q) (e K d : ℝ) (hK : 0 ≤ K)
80     (he : tv p q ≤ e) (hd : ∀ x, dist (v x) (w x) ≤ d)
81     (hlip : ∀ i y z, |loss i y-loss i z| ≤ K*dist y z)
82     (hl : ∀ i y, 0 ≤ loss i y ∧ loss i y ≤ 1) (i : I) :
83     |responseRisk p v loss i-responseRisk q w loss i| ≤ allowance e K d :=
84   decision_error p q v w loss i hp hq e K d hK he hd
85     (fun x => hlip i (v x) (w x)) (fun x => hl i (v x)) (fun x => hl i (w x))
86 
87 /-- A data-dependent allocation of response error can be charged by its expected value. -/
88 theorem expected_response_error [Fintype X] [PseudoMetricSpace V]
89     (p q : X → ℝ) (v w : X → V) (loss : I → V → ℝ) (i : I)
90     (hp : IsDist p) (hq : IsDist q) (e K d : ℝ) (hK : 0 ≤ K)
91     (he : tv p q ≤ e) (hd : (∑ x, dist (v x) (w x)*p x) ≤ d)
92     (hlip : ∀ x, |loss i (v x)-loss i (w x)| ≤ K*dist (v x) (w x))
93     (hv : ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
94     (hw : ∀ x, 0 ≤ loss i (w x) ∧ loss i (w x) ≤ 1) :
95     |responseRisk p v loss i-responseRisk q w loss i| ≤ allowance e K d := by
96   have hresponse : |responseRisk p v loss i-responseRisk p w loss i| ≤ K*d := by
97     calc
98       _ ≤ ∑ x, |loss i (v x)-loss i (w x)| * p x := loss_change_bound p _ _ hp.1
99       _ ≤ ∑ x, (K*dist (v x) (w x))*p x := Finset.sum_le_sum
100         (fun x _ => mul_le_mul_of_nonneg_right (hlip x) (hp.1 x))
101       _ = K * ∑ x, dist (v x) (w x)*p x := by simp only [Finset.mul_sum, mul_assoc]
102       _ ≤ K*d := mul_le_mul_of_nonneg_left hd hK
103   apply le_min
104   · have hv' := response_risk_range p v loss i hp hv
105     have hw' := response_risk_range q w loss i hq hw
106     exact abs_le.mpr ⟨by linarith, by linarith⟩
107   · have hprob := same_policy_error p q (fun x => loss i (w x)) hp hq 1 e (by norm_num) hw he
108     have htri := abs_sub_le (responseRisk p v loss i) (responseRisk p w loss i) (responseRisk q w loss i)
109     change |responseRisk p w loss i-responseRisk q w loss i| ≤ 1*e at hprob
110     linarith
111 
112 /-- Core 4.1's regret claim, against any member of the same action catalogue. -/
113 theorem selected_regret [Fintype X] (p q : X → ℝ) (v w : X → V)
114     (loss : I → V → ℝ) (S : Finset I) (hp : IsDist p) (ξ : ℝ)
115     (hv : ∀ i ∈ S, ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
116     (herr : ∀ i ∈ S, |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ)
117     (chosen best : I) (hc : chosen ∈ S) (hb : best ∈ S)
118     (hopt : ∀ i ∈ S, responseRisk q w loss chosen ≤ responseRisk q w loss i) :
119     responseRisk p v loss chosen-responseRisk p v loss best ≤ min 1 (2*ξ) :=
120   regret_from_uniform_error _ _ S 1 ξ
121     (fun i hi => response_risk_range p v loss i hp (hv i hi)) herr chosen best hc hb hopt
122 
123 /-- Both minimizers exist over the actual finite nonempty catalogue. -/
124 theorem minimizing_decisions_exist [Fintype X] (p q : X → ℝ) (v w : X → V)
125     (loss : I → V → ℝ) (S : Finset I) (hS : S.Nonempty) (hp : IsDist p) (ξ : ℝ)
126     (hv : ∀ i ∈ S, ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
127     (herr : ∀ i ∈ S, |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ) :
128     ∃ chosen ∈ S, ∃ best ∈ S,
129       (∀ i ∈ S, responseRisk q w loss chosen ≤ responseRisk q w loss i) ∧
130       (∀ i ∈ S, responseRisk p v loss best ≤ responseRisk p v loss i) ∧
131       responseRisk p v loss chosen-responseRisk p v loss best ≤ min 1 (2*ξ) := by
132   obtain ⟨c,hc,ec⟩ := Planning.finiteMin_attained S hS (responseRisk q w loss)
133   obtain ⟨b,hb,eb⟩ := Planning.finiteMin_attained S hS (responseRisk p v loss)
134   have hcmin : ∀ i ∈ S, responseRisk q w loss c ≤ responseRisk q w loss i := by
135     intro i hi; rw [ec]; exact Planning.finiteMin_le S hS _ i hi
136   refine ⟨c,hc,b,hb,hcmin,?_,selected_regret p q v w loss S hp ξ hv herr c b hc hb hcmin⟩
137   intro i hi; rw [eb]; exact Planning.finiteMin_le S hS _ i hi
138 
139 /-- Source-form regret against the actual finite minimum, not a supplied optimum value. -/
140 theorem regret_to_minimum [Fintype X] (p q : X → ℝ) (v w : X → V)
141     (loss : I → V → ℝ) (S : Finset I) (hS : S.Nonempty) (hp : IsDist p) (ξ : ℝ)
142     (hv : ∀ i ∈ S, ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
143     (herr : ∀ i ∈ S, |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ)
144     (chosen : I) (hc : chosen ∈ S)
145     (hopt : ∀ i ∈ S, responseRisk q w loss chosen ≤ responseRisk q w loss i) :
146     responseRisk p v loss chosen-Planning.finiteMin S hS (responseRisk p v loss) ≤ min 1 (2*ξ) := by
147   obtain ⟨b,hb,eb⟩ := Planning.finiteMin_attained S hS (responseRisk p v loss)
148   rw [← eb]
149   exact selected_regret p q v w loss S hp ξ hv herr chosen b hc hb hopt
150 
151 /-- All parts of the source estimate supply actual minimizing decisions over a common catalogue. -/
152 theorem metric_minimizers_exist [Fintype X] [PseudoMetricSpace V]
153     (p q : X → ℝ) (v w : X → V) (loss : I → V → ℝ) (S : Finset I) (hS : S.Nonempty)
154     (hp : IsDist p) (hq : IsDist q) (e K d : ℝ) (hK : 0 ≤ K)
155     (he : tv p q ≤ e) (hd : ∀ x, dist (v x) (w x) ≤ d)
156     (hlip : ∀ i ∈ S, ∀ x, |loss i (v x)-loss i (w x)| ≤ K*dist (v x) (w x))
157     (hv : ∀ i ∈ S, ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
158     (hw : ∀ i ∈ S, ∀ x, 0 ≤ loss i (w x) ∧ loss i (w x) ≤ 1) :
159     ∃ chosen ∈ S, ∃ best ∈ S,
160       (∀ i ∈ S, responseRisk q w loss chosen ≤ responseRisk q w loss i) ∧
161       (∀ i ∈ S, responseRisk p v loss best ≤ responseRisk p v loss i) ∧
162       responseRisk p v loss chosen-responseRisk p v loss best ≤ min 1 (2*allowance e K d) :=
163   minimizing_decisions_exist p q v w loss S hS hp (allowance e K d) hv
164     (fun i hi => decision_error p q v w loss i hp hq e K d hK he hd (hlip i hi) (hv i hi) (hw i hi))
165 
166 /-- The strict factor-two gap excludes every other true minimizer. -/
167 theorem unique_minimizer_transfer [Fintype X] (p q : X → ℝ) (v w : X → V)
168     (loss : I → V → ℝ) (S : Finset I) (ξ : ℝ) (chosen : I) (hc : chosen ∈ S)
169     (herr : ∀ i ∈ S, |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ)
170     (hgap : ∀ i ∈ S, i ≠ chosen → responseRisk q w loss chosen+2*ξ < responseRisk q w loss i) :
171     (∀ i ∈ S, i ≠ chosen → responseRisk p v loss chosen < responseRisk p v loss i) ∧
172     (∀ i ∈ S, (∀ j ∈ S, responseRisk p v loss i ≤ responseRisk p v loss j) → i=chosen) := by
173   have hs : ∀ i ∈ S, i ≠ chosen → responseRisk p v loss chosen < responseRisk p v loss i := by
174     intro i hi hne
175     exact robust_gap _ _ chosen i ξ (herr chosen hc) (herr i hi) (hgap i hi hne)
176   refine ⟨hs,?_⟩
177   intro i hi hmin
178   by_contra hne
179   exact (not_le_of_gt (hs i hi hne)) (hmin chosen hc)
180 
181 /-- A bounded risk interval, not a claim that a model covers the physical world. -/
182 theorem risk_interval [Fintype X] (p q : X → ℝ) (v w : X → V)
183     (loss : I → V → ℝ) (i : I) (hp : IsDist p) (ξ : ℝ)
184     (hv : ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
185     (herr : |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ) :
186     max 0 (responseRisk q w loss i-ξ) ≤ responseRisk p v loss i ∧
187     responseRisk p v loss i ≤ min 1 (responseRisk q w loss i+ξ) := by
188   have hr := response_risk_range p v loss i hp hv
189   have he := abs_le.mp herr
190   exact ⟨max_le hr.1 (by linarith), le_min hr.2 (by linarith)⟩
191 
192 theorem risk_threshold [Fintype X] (p q : X → ℝ) (v w : X → V)
193     (loss : I → V → ℝ) (i : I) (ξ τ : ℝ)
194     (herr : |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ)
195     (hpass : responseRisk q w loss i+ξ ≤ τ) : responseRisk p v loss i ≤ τ := by
196   have h := (abs_le.mp herr).2
197   linarith
198 
199 /-- An optimizer with certified additive residual eta has its own additional charge. -/
200 theorem approximate_optimizer_regret [Fintype X] (p q : X → ℝ) (v w : X → V)
201     (loss : I → V → ℝ) (S : Finset I) (hp : IsDist p) (ξ η : ℝ)
202     (hv : ∀ i ∈ S, ∀ x, 0 ≤ loss i (v x) ∧ loss i (v x) ≤ 1)
203     (herr : ∀ i ∈ S, |responseRisk p v loss i-responseRisk q w loss i| ≤ ξ)
204     (chosen best : I) (hc : chosen ∈ S) (hb : best ∈ S)
205     (hopt : ∀ i ∈ S, responseRisk q w loss chosen ≤ responseRisk q w loss i+η) :
206     responseRisk p v loss chosen-responseRisk p v loss best ≤ min 1 (2*ξ+η) := by
207   have h1 := (abs_le.mp (herr chosen hc)).2
208   have h2 := (abs_le.mp (herr best hb)).1
209   have h3 := hopt best hb
210   have hc' := response_risk_range p v loss chosen hp (hv chosen hc)
211   have hb' := response_risk_range p v loss best hp (hv best hb)
212   exact le_min (by linarith) (by linarith)
213 
214 end
215 end Komorebi.MachineTheory.ResponseDecision

Back to source controls