ResponseExamples.lean

1 import MachineTheory.DecisionHistory
2 import MachineTheory.ApproximationExamples
3 
4 /-!
5 Core4.1, checked boundaries and a single sensor record. The example is not a
6 physical observation or a new optimization theorem for the changed instrument.
7 It certifies one terminal decision after one positive report.
8 -/
9 namespace Komorebi.MachineTheory.ResponseExamples
10 open scoped BigOperators
11 open Instrument Variation ApproximateHistory ApproximateDecision ResponseDecision DecisionHistory
12 noncomputable section
13 
14 /-- On the attained unit interval, either select zero or select one. -/
15 def scalarLoss (a : Bool) (y : ℝ) : ℝ := if a then 1-y else y
16 
17 theorem scalarLoss_range (a : Bool) (y : ℝ) (hy : 0 ≤ y ∧ y ≤ 1) :
18     0 ≤ scalarLoss a y ∧ scalarLoss a y ≤ 1 := by
19   cases a <;> simp only [scalarLoss, Bool.false_eq_true, ite_false, ite_true]
20   · exact hy
21   · constructor <;> linarith [hy.1,hy.2]
22 
23 theorem scalarLoss_lipschitz (a : Bool) (y z : ℝ) :
24     |scalarLoss a y-scalarLoss a z| ≤ 1*dist y z := by
25   cases a <;> simp [scalarLoss, Real.dist_eq, abs_sub_comm]
26 
27 abbrev Pair := PlanningSensor.Pair
28 abbrev Outcome := Bool × Pair
29 
30 def trueEvidence : Outcome → ℝ :=
31   push (reportMap PlanningSensor.project)
32     (jointEvidence ApproximationExamples.calibrated37 () PlanningSensor.initialFine.val)
33 
34 def modelEvidence : Outcome → ℝ :=
35   jointEvidence PlanningSensor.sensorLaw () (push PlanningSensor.project PlanningSensor.initialFine.val)
36 
37 def reportOne : Finset Outcome := Finset.univ.filter (fun x => x.1 = true)
38 
39 def truePosterior : Pair → ℝ := recordAfter Prod.snd reportOne trueEvidence
40 
41 def modelPosterior : Pair → ℝ := recordAfter Prod.snd reportOne modelEvidence
42 
43 /-- A deliberately specified finite stored record: exact hundredths, not inferred calibration. -/
44 def storedRecord (z : Pair) : ℝ := if z.1=z.2 then (if z.1 then 19/25 else 6/25) else 0
45 
46 def targetResponse (z : Pair) : ℝ := if z.1 then 1 else 0
47 
48 def approximateResponse (z : Pair) : ℝ := if z.1 then 99/100 else 1/100
49 
50 theorem trueEvidence_dist : IsDist trueEvidence :=
51   push_dist _ _ (jointEvidence_dist _ _ _ PlanningSensor.initialFine.property)
52 
53 theorem modelEvidence_dist : IsDist modelEvidence :=
54   jointEvidence_dist _ _ _ (push_dist _ _ PlanningSensor.initialFine.property)
55 
56 /-- This law bound is derived from the inherited 37/50-versus-3/4 joint-row theorem. -/
57 theorem sensor_evidence_bound : tv trueEvidence modelEvidence ≤ 1/100 := by
58   have h := jointEvidence_error PlanningSensor.project ApproximationExamples.calibrated37
59     PlanningSensor.sensorLaw () PlanningSensor.initialFine.val
60     (push PlanningSensor.project PlanningSensor.initialFine.val) PlanningSensor.initialFine.property
61     0 (1/100) (by rw [tv_self])
62     (fun x => le_of_eq (ApproximationExamples.sensor_joint_row_error () x))
63   simpa only [trueEvidence, modelEvidence, zero_add] using h
64 
65 theorem trueEvidence_value (o b s : Bool) :
66     trueEvidence (o,b,s) = if b=s then (if o=s then 37/100 else 13/100) else 0 := by
67   cases o <;> cases b <;> cases s <;>
68     norm_num [trueEvidence, jointEvidence, jointKernel, jointRow, push, applyKernel,
69       ApproximationExamples.calibrated37, PlanningSensor.initialFine,
70       PlanningSensor.project, reportMap, Fintype.sum_prod_type, Fintype.sum_bool, ite_and]
71 
72 theorem modelEvidence_value (o b s : Bool) :
73     modelEvidence (o,b,s) = if b=s then (if o=s then 3/8 else 1/8) else 0 := by
74   cases o <;> cases b <;> cases s <;>
75     norm_num [modelEvidence, jointEvidence, jointKernel, jointRow, push, applyKernel,
76       PlanningSensor.sensorLaw, PlanningSensor.accuracy, PlanningSensor.initialFine,
77       PlanningSensor.project, Fintype.sum_prod_type, Fintype.sum_bool, ite_and]
78 
79 theorem sensor_report_masses : mass (restrict reportOne trueEvidence) = 1/2 ∧
80     mass (restrict reportOne modelEvidence) = 1/2 := by
81   norm_num [mass, restrict, reportOne, Fintype.sum_prod_type, Fintype.sum_bool,
82     trueEvidence_value, modelEvidence_value]
83 
84 theorem truePosterior_value (b s : Bool) :
85     truePosterior (b,s) = if b=s then (if b then 37/50 else 13/50) else 0 := by
86   cases b <;> cases s <;>
87     norm_num [truePosterior, recordAfter, push, normalize, restrict, reportOne, mass,
88       Fintype.sum_prod_type, Fintype.sum_bool, trueEvidence_value, ite_and]
89 
90 theorem modelPosterior_value (b s : Bool) :
91     modelPosterior (b,s) = if b=s then (if b then 3/4 else 1/4) else 0 := by
92   cases b <;> cases s <;>
93     norm_num [modelPosterior, recordAfter, push, normalize, restrict, reportOne, mass,
94       Fintype.sum_prod_type, Fintype.sum_bool, modelEvidence_value, ite_and]
95 
96 theorem truePosterior_dist : IsDist truePosterior :=
97   recordAfter_dist Prod.snd reportOne trueEvidence trueEvidence_dist
98     (by rw [sensor_report_masses.1]; norm_num)
99 
100 theorem modelPosterior_dist : IsDist modelPosterior :=
101   recordAfter_dist Prod.snd reportOne modelEvidence modelEvidence_dist
102     (by rw [sensor_report_masses.2]; norm_num)
103 
104 theorem storedRecord_dist : IsDist storedRecord := by
105   constructor
106   · rintro ⟨b,s⟩; cases b <;> cases s <;> norm_num [storedRecord]
107   · norm_num [mass, storedRecord, Fintype.sum_prod_type, Fintype.sum_bool]
108 
109 theorem stored_record_error : tv modelPosterior storedRecord = 1/100 := by
110   norm_num [tv, l1, Fintype.sum_prod_type, Fintype.sum_bool, modelPosterior_value, storedRecord]
111 
112 /-- The true-model discrepancy is not replaced by this sharper, after-the-fact arithmetic. -/
113 theorem actual_record_error : tv truePosterior storedRecord = 1/50 := by
114   norm_num [tv, l1, Fintype.sum_prod_type, Fintype.sum_bool, truePosterior_value, storedRecord]
115 
116 theorem response_error (z : Pair) : dist (targetResponse z) (approximateResponse z) = 1/100 := by
117   rcases z with ⟨b,s⟩; cases b <;> norm_num [targetResponse, approximateResponse, Real.dist_eq]
118 
119 theorem target_range (z : Pair) : 0 ≤ targetResponse z ∧ targetResponse z ≤ 1 := by
120   rcases z with ⟨b,s⟩; cases b <;> norm_num [targetResponse]
121 
122 theorem approximate_range (z : Pair) : 0 ≤ approximateResponse z ∧ approximateResponse z ≤ 1 := by
123   rcases z with ⟨b,s⟩; cases b <;> norm_num [approximateResponse]
124 
125 theorem composed_allowance :
126     allowance (recordAllowance reportOne trueEvidence modelEvidence (1/100) (1/100)) 1 (1/100) = 1/25 := by
127   unfold allowance recordAllowance
128   rw [sensor_report_masses.1, sensor_report_masses.2]
129   norm_num
130 
131 /-- The certificate uses the full chain of proved allowances, not the exact observed error. -/
132 theorem sensor_decision_error (a : Bool) :
133     |responseRisk truePosterior targetResponse scalarLoss a-
134       responseRisk storedRecord approximateResponse scalarLoss a| ≤ 1/25 := by
135   rw [← composed_allowance]
136   exact conditioned_response_error Prod.snd reportOne trueEvidence modelEvidence storedRecord
137     trueEvidence_dist modelEvidence_dist storedRecord_dist
138     (by rw [sensor_report_masses.1]; norm_num) (by rw [sensor_report_masses.2]; norm_num)
139     (1/100) (1/100) sensor_evidence_bound (le_of_eq stored_record_error)
140     targetResponse approximateResponse scalarLoss a 1 (1/100) (by norm_num)
141     (fun z => le_of_eq (response_error z)) (fun z => scalarLoss_lipschitz a _ _)
142     (fun z => scalarLoss_range a _ (target_range z))
143     (fun z => scalarLoss_range a _ (approximate_range z))
144 
145 theorem sensor_risk_values :
146     responseRisk truePosterior targetResponse scalarLoss true = 13/50 ∧
147     responseRisk truePosterior targetResponse scalarLoss false = 37/50 ∧
148     responseRisk storedRecord approximateResponse scalarLoss true = 613/2500 ∧
149     responseRisk storedRecord approximateResponse scalarLoss false = 1887/2500 := by
150   norm_num [responseRisk, risk, Fintype.sum_prod_type, Fintype.sum_bool,
151     truePosterior_value, storedRecord, targetResponse, approximateResponse, scalarLoss]
152 
153 theorem sensor_true_unique_from_certificate :
154     ∀ a : Bool, a ≠ true → responseRisk truePosterior targetResponse scalarLoss true <
155       responseRisk truePosterior targetResponse scalarLoss a := by
156   have h := unique_minimizer_transfer truePosterior storedRecord targetResponse approximateResponse
157     scalarLoss Finset.univ (1/25) true (Finset.mem_univ _) (fun a _ => sensor_decision_error a)
158     (by intro a _ hne; cases a <;> simp_all [sensor_risk_values.2.2.1, sensor_risk_values.2.2.2]; norm_num)
159   intro a hne
160   exact h.1 a (Finset.mem_univ _) hne
161 
162 theorem sensor_risk_upper_certificate :
163     responseRisk truePosterior targetResponse scalarLoss true ≤ 713/2500 := by
164   apply risk_threshold truePosterior storedRecord targetResponse approximateResponse scalarLoss true
165     (1/25) (713/2500) (sensor_decision_error true)
166   rw [sensor_risk_values.2.2.1]
167   norm_num
168 
169 theorem sensor_threshold_certificate :
170     responseRisk truePosterior targetResponse scalarLoss true ≤ 3/10 :=
171   sensor_risk_upper_certificate.trans (by norm_num)
172 
173 theorem sensor_error_and_margin :
174     |responseRisk truePosterior targetResponse scalarLoss true-
175       responseRisk storedRecord approximateResponse scalarLoss true| = 37/2500 ∧
176     responseRisk storedRecord approximateResponse scalarLoss true+2*(1/25) <
177       responseRisk storedRecord approximateResponse scalarLoss false := by
178   rw [sensor_risk_values.1, sensor_risk_values.2.2.1, sensor_risk_values.2.2.2]
179   norm_num
180 
181 /-- Exact probabilities alone do not justify an inaccurate response. -/
182 theorem response_term_is_necessary :
183     tv (basis () : Unit → ℝ) (basis ()) = 0 ∧
184     |responseRisk (basis () : Unit → ℝ) (fun _ => (0 : ℝ)) scalarLoss false-
185       responseRisk (basis () : Unit → ℝ) (fun _ => (1/5 : ℝ)) scalarLoss false| = 1/5 := by
186   norm_num [tv, l1, responseRisk, risk, basis, scalarLoss]
187 
188 /-- Accurate responses do not compensate for an incorrect probability record. -/
189 theorem probability_term_is_necessary :
190     tv (basis false : Bool → ℝ) (basis true) = 1 ∧
191     |responseRisk (basis false) (fun b : Bool => if b then (1 : ℝ) else 0) scalarLoss false-
192       responseRisk (basis true) (fun b : Bool => if b then (1 : ℝ) else 0) scalarLoss false| = 1 := by
193   norm_num [tv, l1, responseRisk, risk, basis, scalarLoss, Fintype.sum_bool]
194 
195 /-- At exactly twice the error, a unique approximate choice can become a true tie. -/
196 theorem gap_equality_is_not_uniqueness :
197     responseRisk (basis () : Unit → ℝ) (fun _ => (2/5 : ℝ)) scalarLoss false+2*(1/10) =
198       responseRisk (basis () : Unit → ℝ) (fun _ => (2/5 : ℝ)) scalarLoss true ∧
199     responseRisk (basis () : Unit → ℝ) (fun _ => (1/2 : ℝ)) scalarLoss false =
200       responseRisk (basis () : Unit → ℝ) (fun _ => (1/2 : ℝ)) scalarLoss true := by
201   norm_num [responseRisk, risk, basis, scalarLoss]
202 
203 /-- A smaller approximate gap can actually reverse the decision. -/
204 theorem small_gap_reverses :
205     responseRisk (basis () : Unit → ℝ) (fun _ => (9/20 : ℝ)) scalarLoss false <
206       responseRisk (basis () : Unit → ℝ) (fun _ => (9/20 : ℝ)) scalarLoss true ∧
207     responseRisk (basis () : Unit → ℝ) (fun _ => (11/20 : ℝ)) scalarLoss true <
208       responseRisk (basis () : Unit → ℝ) (fun _ => (11/20 : ℝ)) scalarLoss false := by
209   norm_num [responseRisk, risk, basis, scalarLoss]
210 
211 /-- Same laws and responses, different objectives: this is not an approximation chain. -/
212 theorem changed_loss_is_unaccounted :
213     |responseRisk (basis () : Unit → ℝ) (fun _ => (0 : ℝ)) (fun (_ : Unit) _ => (0 : ℝ)) ()-
214       responseRisk (basis () : Unit → ℝ) (fun _ => (0 : ℝ)) (fun (_ : Unit) _ => (1 : ℝ)) ()| = 1 := by
215   norm_num [responseRisk, risk, basis]
216 
217 /-- A bounded discontinuous loss need not have unit sensitivity. -/
218 theorem bounded_is_not_lipschitz_one :
219     dist (0 : ℝ) (1/100) = 1/100 ∧
220     |(if (0 : ℝ)>0 then (1 : ℝ) else 0)-(if (1/100 : ℝ)>0 then (1 : ℝ) else 0)| = 1 := by
221   norm_num [Real.dist_eq]
222 
223 /-- The loss range is necessary for the cap one and the coefficient on total variation. -/
224 theorem unbounded_loss_breaks_cap :
225     risk (basis false : Bool → ℝ) (fun b => if b then 10 else 0) = 0 ∧
226     risk (basis true : Bool → ℝ) (fun b => if b then 10 else 0) = 10 := by
227   norm_num [risk, basis, Fintype.sum_bool]
228 
229 /-- Perfect numerical estimation does not certify a deliberately nonoptimal selected action. -/
230 theorem optimization_residual_cannot_disappear :
231     responseRisk (basis () : Unit → ℝ) (fun _ => (1/4 : ℝ)) scalarLoss true-
232       responseRisk (basis () : Unit → ℝ) (fun _ => (1/4 : ℝ)) scalarLoss false = 1/2 := by
233   norm_num [responseRisk, risk, basis, scalarLoss]
234 
235 /-- An impossible event is excluded before the conditional decision theorem is used. -/
236 theorem impossible_report_has_no_probability_record :
237     mass (restrict (∅ : Finset Bool) (basis false)) = 0 ∧
238     ¬ IsDist (recordAfter id (∅ : Finset Bool) (basis false)) := by
239   norm_num [IsDist, recordAfter, mass, push, normalize, restrict, Fintype.sum_bool]
240 
241 end
242 end Komorebi.MachineTheory.ResponseExamples

Back to source controls