ApproximateDecision.lean

1 import MachineTheory.ApproximateHistory
2 import MachineTheory.Planning
3 
4 /-!
5 Core 5.6: a uniform same-policy law bound controls selection of a different policy.
6 The loss for each policy is the same bounded function in the two models. The finite
7 policy catalogue is shared. Admissibility, absorbing-stop encoding and model truth
8 are separate premises, not consequences of an expected-loss bound.
9 -/
10 namespace Komorebi.MachineTheory.ApproximateDecision
11 open scoped BigOperators
12 open Instrument Variation ApproximateHistory
13 noncomputable section
14 variable {X I : Type*}
15 
16 def risk [Fintype X] (p f : X → ℝ) : ℝ := ∑ x, f x * p x
17 
18 theorem risk_range [Fintype X] (p f : X → ℝ) (hp : IsDist p) (B : ℝ)
19     (hf : ∀ x, 0 ≤ f x ∧ f x ≤ B) : 0 ≤ risk p f ∧ risk p f ≤ B := by
20   constructor
21   · exact Finset.sum_nonneg (fun x _ => mul_nonneg (hf x).1 (hp.1 x))
22   · calc
23       risk p f ≤ ∑ x, B*p x := Finset.sum_le_sum
24         (fun x _ => mul_le_mul_of_nonneg_right (hf x).2 (hp.1 x))
25       _ = B := by rw [← Finset.mul_sum]; change B*mass p=B; rw [hp.2, mul_one]
26 
27 /-- The fixed-policy comparison is established before policy selection is used. -/
28 theorem same_policy_error [Fintype X] (p q f : X → ℝ)
29     (hp : IsDist p) (hq : IsDist q) (B d : ℝ) (hB : 0 ≤ B)
30     (hf : ∀ x, 0 ≤ f x ∧ f x ≤ B) (hd : tv p q ≤ d) :
31     |risk p f-risk q f| ≤ B*d :=
32   (expectation_bound p q f (hp.2.trans hq.2.symm) B hB hf).trans
33     (mul_le_mul_of_nonneg_left hd hB)
34 
35 /-- An explicit lower/upper error interval on each of the same fixed alternatives. -/
36 theorem regret_from_uniform_error (J Q : I → ℝ) (S : Finset I) (B e : ℝ)
37     (hJ : ∀ i ∈ S, 0 ≤ J i ∧ J i ≤ B)
38     (he : ∀ i ∈ S, |J i-Q i| ≤ e)
39     (chosen comparator : I) (hc : chosen ∈ S) (hr : comparator ∈ S)
40     (hopt : ∀ i ∈ S, Q chosen ≤ Q i) :
41     J chosen-J comparator ≤ min B (2*e) := by
42   apply le_min
43   · linarith [(hJ chosen hc).2, (hJ comparator hr).1]
44   · have h1 := (abs_le.mp (he chosen hc)).2
45     have h2 := (abs_le.mp (he comparator hr)).1
46     have h3 := hopt comparator hr
47     linarith
48 
49 /-- Core 5.6, including its range cap, for any declared common finite class. -/
50 theorem uniform_policy_regret [Fintype X]
51     (P Q : I → X → ℝ) (loss : I → X → ℝ) (S : Finset I) (B d : ℝ) (hB : 0 ≤ B)
52     (hP : ∀ i ∈ S, IsDist (P i)) (hQ : ∀ i ∈ S, IsDist (Q i))
53     (hL : ∀ i ∈ S, ∀ x, 0 ≤ loss i x ∧ loss i x ≤ B)
54     (hD : ∀ i ∈ S, tv (P i) (Q i) ≤ d)
55     (chosen comparator : I) (hc : chosen ∈ S) (hr : comparator ∈ S)
56     (hopt : ∀ i ∈ S, risk (Q chosen) (loss chosen) ≤ risk (Q i) (loss i)) :
57     risk (P chosen) (loss chosen)-risk (P comparator) (loss comparator) ≤ min B (2*B*d) := by
58   have h := regret_from_uniform_error
59     (fun i => risk (P i) (loss i)) (fun i => risk (Q i) (loss i)) S B (B*d)
60     (fun i hi => risk_range (P i) (loss i) (hP i hi) B (hL i hi))
61     (fun i hi => same_policy_error (P i) (Q i) (loss i) (hP i hi) (hQ i hi) B d hB (hL i hi) (hD i hi))
62     chosen comparator hc hr hopt
63   simpa only [mul_assoc] using h
64 
65 /-- The finite common class actually has both minimizers. -/
66 theorem minimizing_policies_exist [Fintype X]
67     (P Q : I → X → ℝ) (loss : I → X → ℝ) (S : Finset I) (hS : S.Nonempty)
68     (B d : ℝ) (hB : 0 ≤ B)
69     (hP : ∀ i ∈ S, IsDist (P i)) (hQ : ∀ i ∈ S, IsDist (Q i))
70     (hL : ∀ i ∈ S, ∀ x, 0 ≤ loss i x ∧ loss i x ≤ B)
71     (hD : ∀ i ∈ S, tv (P i) (Q i) ≤ d) :
72     ∃ chosen ∈ S, ∃ best ∈ S,
73       (∀ i ∈ S, risk (Q chosen) (loss chosen) ≤ risk (Q i) (loss i)) ∧
74       (∀ i ∈ S, risk (P best) (loss best) ≤ risk (P i) (loss i)) ∧
75       risk (P chosen) (loss chosen)-risk (P best) (loss best) ≤ min B (2*B*d) := by
76   obtain ⟨chosen,hc,eqc⟩ := Planning.finiteMin_attained S hS (fun i => risk (Q i) (loss i))
77   obtain ⟨best,hb,eqb⟩ := Planning.finiteMin_attained S hS (fun i => risk (P i) (loss i))
78   have hmin : ∀ i ∈ S, risk (Q chosen) (loss chosen) ≤ risk (Q i) (loss i) := by
79     intro i hi; rw [eqc]; exact Planning.finiteMin_le S hS _ i hi
80   refine ⟨chosen,hc,best,hb,hmin,?_,uniform_policy_regret P Q loss S B d hB hP hQ hL hD chosen best hc hb hmin⟩
81   intro i hi; rw [eqb]; exact Planning.finiteMin_le S hS _ i hi
82 
83 /-- A strict approximate gap larger than twice the error preserves the true comparison. -/
84 theorem robust_gap (J Q : I → ℝ) (i j : I) (e : ℝ)
85     (hi : |J i-Q i| ≤ e) (hj : |J j-Q j| ≤ e) (gap : Q i+2*e < Q j) : J i < J j := by
86   have h1 := (abs_le.mp hi).2
87   have h2 := (abs_le.mp hj).1
88   linarith
89 
90 universe u
91 variable {S Z A O : Type u}
92 
93 /-- The first half of Core 5.6 is instantiated by the whole-history theorem, uniformly in the policy. -/
94 theorem history_policy_error [Fintype S] [Fintype Z] [Fintype A] [Fintype O]
95     [DecidableEq S] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
96     (π : S → Z) (K : Nat → Law S A O) (L : Nat → Law Z A O)
97     (g : Policy A O) (p : S → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
98     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
99     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
100     (H : Nat) (loss : Path Z A O H → ℝ) (B : ℝ) (hB : 0 ≤ B)
101     (hL : ∀ h, 0 ≤ loss h ∧ loss h ≤ B) :
102     |risk (push (project π H) (law K g p H)) loss-risk (law L g q H) loss| ≤
103       B * min 1 (δ + ∑ n ∈ Finset.range H, ε n) :=
104   same_policy_error _ _ _ (push_dist _ _ (law_dist K g p hp H)) (law_dist L g q hq H)
105     B _ hB hL (whole_history_bound π K L g p q hp hq δ ε h0 hε H)
106 
107 /-- Two separately chosen policies are compared only after every fixed policy has been transported. -/
108 theorem history_selected_policy_regret [Fintype S] [Fintype Z] [Fintype A] [Fintype O]
109     [DecidableEq S] [DecidableEq Z] [DecidableEq A] [DecidableEq O]
110     (π : S → Z) (K : Nat → Law S A O) (L : Nat → Law Z A O)
111     (policies : I → Policy A O) (catalogue : Finset I)
112     (p : S → ℝ) (q : Z → ℝ) (hp : IsDist p) (hq : IsDist q)
113     (δ : ℝ) (ε : Nat → ℝ) (h0 : tv (push π p) q ≤ δ)
114     (hε : ∀ n a x, tv (push (reportMap π) (jointRow (K n) a x)) (jointRow (L n) a (π x)) ≤ ε n)
115     (H : Nat) (loss : I → Path Z A O H → ℝ) (B : ℝ) (hB : 0 ≤ B)
116     (hL : ∀ i ∈ catalogue, ∀ h, 0 ≤ loss i h ∧ loss i h ≤ B)
117     (chosen best : I) (hc : chosen ∈ catalogue) (hb : best ∈ catalogue)
118     (hopt : ∀ i ∈ catalogue, risk (law L (policies chosen) q H) (loss chosen) ≤ risk (law L (policies i) q H) (loss i)) :
119     risk (push (project π H) (law K (policies chosen) p H)) (loss chosen) -
120       risk (push (project π H) (law K (policies best) p H)) (loss best) ≤
121       min B (2*B*min 1 (δ + ∑ n ∈ Finset.range H, ε n)) :=
122   uniform_policy_regret
123     (fun i => push (project π H) (law K (policies i) p H))
124     (fun i => law L (policies i) q H) loss catalogue B _ hB
125     (fun i _ => push_dist _ _ (law_dist K (policies i) p hp H))
126     (fun i _ => law_dist L (policies i) q hq H) hL
127     (fun i _ => whole_history_bound π K L (policies i) p q hp hq δ ε h0 hε H)
128     chosen best hc hb hopt
129 
130 end
131 end Komorebi.MachineTheory.ApproximateDecision

Back to source controls