ApproximationExamples.lean

1 import MachineTheory.ApproximateDecision
2 import MachineTheory.PlanningSensor
3 
4 /-!
5 Exact boundary examples. These are proof terms over specified probability laws,
6 not sampled observations, confidence intervals, or oracle-provided counter values.
7 -/
8 namespace Komorebi.MachineTheory.ApproximationExamples
9 open scoped BigOperators
10 open Instrument Variation ApproximateHistory ApproximateDecision
11 noncomputable section
12 
13 abbrev Outcome := Bool × Bool
14 
15 /-- First bit marks the rare report; second bit is the output of interest. -/
16 def rareP (δ : ℝ) : Outcome → ℝ
17   | (false,false) => 1-δ
18   | (true,false) => δ
19   | _ => 0
20 
21 def rareQ (δ : ℝ) : Outcome → ℝ
22   | (false,false) => 1-δ
23   | (true,true) => δ
24   | _ => 0
25 
26 def rareEvent : Finset Outcome := {(true,false),(true,true)}
27 
28 theorem rareP_dist (δ : ℝ) (h0 : 0 ≤ δ) (h1 : δ ≤ 1) : IsDist (rareP δ) := by
29   constructor
30   · rintro ⟨a,b⟩; cases a <;> cases b <;> simp [rareP] <;> linarith
31   · norm_num [mass, Fintype.sum_prod_type, Fintype.sum_bool, rareP]
32 
33 theorem rareQ_dist (δ : ℝ) (h0 : 0 ≤ δ) (h1 : δ ≤ 1) : IsDist (rareQ δ) := by
34   constructor
35   · rintro ⟨a,b⟩; cases a <;> cases b <;> simp [rareQ] <;> linarith
36   · norm_num [mass, Fintype.sum_prod_type, Fintype.sum_bool, rareQ]
37 
38 theorem rare_distance (δ : ℝ) (h0 : 0 ≤ δ) : tv (rareP δ) (rareQ δ) = δ := by
39   simp [tv, l1, Fintype.sum_prod_type, rareP, rareQ, abs_of_nonneg h0]
40 
41 theorem rare_masses (δ : ℝ) : mass (restrict rareEvent (rareP δ)) = δ ∧
42     mass (restrict rareEvent (rareQ δ)) = δ := by
43   norm_num [mass, restrict, rareEvent, Fintype.sum_prod_type, Fintype.sum_bool, rareP, rareQ]
44 
45 theorem rare_posteriors (δ : ℝ) (hδ : 0 < δ) :
46     normalize (restrict rareEvent (rareP δ)) = basis (true,false) ∧
47     normalize (restrict rareEvent (rareQ δ)) = basis (true,true) := by
48   constructor
49   · funext x; rcases x with ⟨a,b⟩
50     unfold normalize; rw [(rare_masses δ).1]
51     cases a <;> cases b <;> simp [restrict, rareEvent, rareP, basis, ne_of_gt hδ]
52   · funext x; rcases x with ⟨a,b⟩
53     unfold normalize; rw [(rare_masses δ).2]
54     cases a <;> cases b <;> simp [restrict, rareEvent, rareQ, basis, ne_of_gt hδ]
55 
56 /-- The event-probability denominator is necessary even for exact finite distributions. -/
57 theorem rare_conditional_distance (δ : ℝ) (hδ : 0 < δ) :
58     tv (normalize (restrict rareEvent (rareP δ))) (normalize (restrict rareEvent (rareQ δ))) = 1 := by
59   rw [(rare_posteriors δ hδ).1, (rare_posteriors δ hδ).2]
60   norm_num [tv, l1, basis, Fintype.sum_prod_type, Fintype.sum_bool]
61 
62 theorem rare_output_distance (δ : ℝ) (hδ : 0 < δ) :
63     tv (push Prod.snd (normalize (restrict rareEvent (rareP δ))))
64       (push Prod.snd (normalize (restrict rareEvent (rareQ δ)))) = 1 := by
65   rw [(rare_posteriors δ hδ).1, (rare_posteriors δ hδ).2]
66   norm_num [tv, l1, push, basis, Fintype.sum_prod_type, Fintype.sum_bool]
67   decide
68 
69 theorem no_unconditioned_posterior_bound :
70     ¬ tv (normalize (restrict rareEvent (rareP (1/100))))
71       (normalize (restrict rareEvent (rareQ (1/100)))) ≤ tv (rareP (1/100)) (rareQ (1/100)) := by
72   rw [rare_conditional_distance _ (by norm_num), rare_distance _ (by norm_num)]
73   norm_num
74 
75 /-- Unequal masses attain the stronger maximum-denominator form. -/
76 def largerEventQ (δ : ℝ) : Outcome → ℝ
77   | (false,false) => 1-2*δ
78   | (true,false) => δ
79   | (true,true) => δ
80   | _ => 0
81 
82 theorem largerEventQ_dist (δ : ℝ) (h0 : 0 ≤ δ) (h1 : δ ≤ 1/2) : IsDist (largerEventQ δ) := by
83   constructor
84   · rintro ⟨a,b⟩; cases a <;> cases b <;> simp [largerEventQ] <;> linarith
85   · norm_num [mass, Fintype.sum_prod_type, Fintype.sum_bool, largerEventQ]; ring
86 
87 theorem unequal_mass_sharp :
88     tv (rareP (1/10)) (largerEventQ (1/10)) = 1/10 ∧
89     mass (restrict rareEvent (rareP (1/10))) = 1/10 ∧
90     mass (restrict rareEvent (largerEventQ (1/10))) = 1/5 ∧
91     tv (normalize (restrict rareEvent (rareP (1/10))))
92       (normalize (restrict rareEvent (largerEventQ (1/10)))) = 1/2 := by
93   norm_num [tv, l1, normalize, mass, restrict, rareEvent, rareP, largerEventQ,
94     Fintype.sum_prod_type, Fintype.sum_bool]
95 
96 /-- The strict threshold for inferring positive counterpart mass cannot be weakened to equality. -/
97 theorem positive_threshold_is_strict :
98     IsDist (rareP (1/10)) ∧ IsDist (rareP 0) ∧
99     tv (rareP (1/10)) (rareP 0) = 1/10 ∧
100     mass (restrict rareEvent (rareP (1/10))) = 1/10 ∧
101     mass (restrict rareEvent (rareP 0)) = 0 := by
102   refine ⟨rareP_dist _ (by norm_num) (by norm_num), rareP_dist _ (by norm_num) (by norm_num), ?_⟩
103   norm_num [tv, l1, mass, restrict, rareEvent, rareP, Fintype.sum_prod_type, Fintype.sum_bool]
104 
105 /-- The factor two in changed-policy regret can be attained because approximate ties can be resolved badly. -/
106 def truthLaw (b : Bool) : ℝ := if b then 3/4 else 1/4
107 
108 def modelLaw (_b : Bool) : ℝ := 1/2
109 
110 def classificationLoss (decision state : Bool) : ℝ := if decision=state then 0 else 1
111 
112 theorem truthLaw_dist : IsDist truthLaw := by
113   constructor
114   · intro b; cases b <;> norm_num [truthLaw]
115   · norm_num [mass, Fintype.sum_bool, truthLaw]
116 
117 theorem modelLaw_dist : IsDist modelLaw := by
118   constructor
119   · intro b; norm_num [modelLaw]
120   · norm_num [mass, Fintype.sum_bool, modelLaw]
121 
122 theorem classification_values :
123     risk truthLaw (classificationLoss false) = 3/4 ∧
124     risk truthLaw (classificationLoss true) = 1/4 ∧
125     risk modelLaw (classificationLoss false) = 1/2 ∧
126     risk modelLaw (classificationLoss true) = 1/2 ∧ tv truthLaw modelLaw = 1/4 := by
127   norm_num [risk, classificationLoss, truthLaw, modelLaw, tv, l1, Fintype.sum_bool]
128 
129 theorem approximate_choice_is_optimal : ∀ d, risk modelLaw (classificationLoss false) ≤ risk modelLaw (classificationLoss d) := by
130   intro d; cases d <;> norm_num [risk, classificationLoss, modelLaw, Fintype.sum_bool]
131 
132 theorem true_choice_is_optimal : ∀ d, risk truthLaw (classificationLoss true) ≤ risk truthLaw (classificationLoss d) := by
133   intro d; cases d <;> norm_num [risk, classificationLoss, truthLaw, Fintype.sum_bool]
134 
135 theorem regret_factor_two_sharp :
136     risk truthLaw (classificationLoss false)-risk truthLaw (classificationLoss true) = 2*tv truthLaw modelLaw := by
137   rw [classification_values.1, classification_values.2.1, classification_values.2.2.2.2]
138   norm_num
139 
140 /-- A same-policy law bound is not a comparison between two different selected losses. -/
141 theorem same_law_not_same_policy_value :
142     tv truthLaw truthLaw = 0 ∧ risk truthLaw (classificationLoss false)-risk truthLaw (classificationLoss true) = 1/2 := by
143   rw [tv_self, classification_values.1, classification_values.2.1]
144   norm_num
145 
146 /-- The delivered regret theorem is instantiated, not only numerically quoted. -/
147 theorem checked_selected_regret :
148     risk truthLaw (classificationLoss false)-risk truthLaw (classificationLoss true) ≤ min 1 (2*1*(1/4)) := by
149   apply uniform_policy_regret (fun _ : Bool => truthLaw) (fun _ : Bool => modelLaw)
150     classificationLoss Finset.univ 1 (1/4) (by norm_num)
151     (fun _ _ => truthLaw_dist) (fun _ _ => modelLaw_dist)
152   · intro d _ b; unfold classificationLoss; split_ifs <;> norm_num
153   · intro _ _; exact le_of_eq classification_values.2.2.2.2
154   · exact Finset.mem_univ _
155   · exact Finset.mem_univ _
156   · intro i _; exact approximate_choice_is_optimal i
157 
158 /-- Source sensor: slightly misspecified calibration, while the hidden world is unchanged. -/
159 def calibrated37 : Law PlanningSensor.World Unit Bool where
160   kernel _ o y x := if y=x then (if o=x.2.1 then 37/50 else 13/50) else 0
161   nonnegative _ _ _ _ := by split_ifs <;> norm_num
162   normalized _ x := by
163     simp only [Finset.sum_ite_eq', Finset.mem_univ, ite_true]
164     rcases x with ⟨b,s,n⟩
165     cases s <;> norm_num [Fintype.sum_bool]
166 
167 /-- Actual coarse report/state row error, not an isolated likelihood entry. -/
168 theorem sensor_joint_row_error (a : Unit) (x : PlanningSensor.World) :
169     tv (push (reportMap PlanningSensor.project) (jointRow calibrated37 a x))
170       (jointRow PlanningSensor.sensorLaw a (PlanningSensor.project x)) = 1/100 := by
171   rcases x with ⟨b,s,n⟩
172   cases b <;> cases s <;> cases n <;>
173     norm_num [tv, l1, push, reportMap, jointRow, calibrated37, PlanningSensor.sensorLaw,
174       PlanningSensor.project, PlanningSensor.accuracy, Fintype.sum_prod_type, Fintype.sum_bool, ite_and]
175 
176 /-- The source's 1/100 per-report discrepancy accumulates on all recorded histories. -/
177 theorem sensor_all_history_error (g : Policy Unit Bool) (p : PlanningSensor.World → ℝ)
178     (hp : IsDist p) (H : Nat) :
179     tv (push (project PlanningSensor.project H) (law (fun _ => calibrated37) g p H))
180       (law (fun _ => PlanningSensor.sensorLaw) g (push PlanningSensor.project p) H) ≤ min 1 ((H : ℝ)/100) := by
181   have h := whole_history_bound PlanningSensor.project (fun _ => calibrated37)
182     (fun _ => PlanningSensor.sensorLaw) g p (push PlanningSensor.project p) hp
183     (push_dist _ _ hp) 0 (fun _ => 1/100) (by rw [tv_self])
184     (fun _ a x => le_of_eq (sensor_joint_row_error a x)) H
185   simpa [Finset.sum_const, Finset.card_range, nsmul_eq_mul, div_eq_mul_inv] using h
186 
187 /-- Core 5.6's displayed sensor margin is exact rational arithmetic. -/
188 theorem sensor_uniform_margins :
189     (23/20 : ℝ) * min 1 ((3 : ℝ)/100) = 69/2000 ∧
190     min (23/20 : ℝ) (2*(23/20)*min 1 ((3 : ℝ)/100)) = 69/1000 := by norm_num
191 
192 /-- One correctly audited alternative does not give a uniform bound on the chosen one. -/
193 theorem baseline_only_audit_fails :
194     tv (basis false : Bool → ℝ) (basis false) = 0 ∧
195     tv (basis true : Bool → ℝ) (basis false) = 1 ∧
196     risk (basis true) (fun b : Bool => if b then 1 else 0) -
197       risk (basis false) (fun b : Bool => if b then 1 else 0) = 1 := by
198   norm_num [tv, l1, basis, risk, Fintype.sum_bool]
199 
200 /-- Resetting the state cannot erase the old state from a complete path record. -/
201 def resetLaw : Law Bool Unit Unit where
202   kernel _ _ y _ := if y=false then 1 else 0
203   nonnegative _ _ _ _ := by split_ifs <;> norm_num
204   normalized _ _ := by simp
205 
206 def unitPolicy : Policy Unit Unit where
207   probability _ _ := 1
208   nonnegative _ _ := by norm_num
209   normalized _ := by simp
210 
211 theorem reset_path_one (p : Bool → ℝ) (b o : Bool) :
212     law (fun _ => resetLaw) unitPolicy p 1 (b,(),(),o) = (if o=false then 1 else 0)*p b := by
213   simpa only [unitPolicy, resetLaw, law_zero, observed, last, one_mul] using
214     (law_succ (fun _ => resetLaw) unitPolicy p 0 b ((),(),o))
215 
216 theorem reset_full_history_distance :
217     tv (law (fun _ => resetLaw) unitPolicy (basis false) 1)
218       (law (fun _ => resetLaw) unitPolicy (basis true) 1) = 1 := by
219   norm_num [tv, l1, Fintype.sum_prod_type, Fintype.sum_bool, law, applyKernel, pathKernel, push, stepRow, jointRow, resetLaw, unitPolicy, basis, last, observed, Path, ite_and]
220 
221 theorem reset_final_states_agree :
222     push (last 1) (law (fun _ => resetLaw) unitPolicy (basis false) 1) =
223       push (last 1) (law (fun _ => resetLaw) unitPolicy (basis true) 1) := by
224   funext b
225   cases b <;> norm_num [push, Fintype.sum_prod_type, Fintype.sum_bool, law, applyKernel, pathKernel, push, stepRow, jointRow, resetLaw, unitPolicy, basis, last, observed, Path, ite_and]
226 
227 end
228 end Komorebi.MachineTheory.ApproximationExamples

Back to source controls