BudgetRobustness.lean

1 import KomorebiSpace.BudgetDuality
2 
3 /-!
4 # Robustness of the fixed-budget profile (WR05)
5 
6 The candidate error estimate holds on one fixed correction space. Evaluating at
7 attaining minimizers gives the two-sided profile bound, and the nominal dual
8 inequality yields a robust lower certificate. No moving-kernel claim is made.
9 -/
10 
11 set_option autoImplicit false
12 
13 noncomputable section
14 namespace KomorebiSpace.BudgetRobustness
15 
16 open scoped RealInnerProductSpace
17 
18 variable {H Y : Type*}
19 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H]
20 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y]
21 
22 /-- Perturbing both the datum and operator changes the residual at a fixed
23 candidate by at most the data error plus the model error times its norm. -/
24 theorem candidate_residual_difference_bound
25     (T S : H →L[ℝ] Y) (r s : Y) {η δ : ℝ}
26     (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ) (a : H) :
27     ‖(r - T a) - (s - S a)‖ ≤ δ + η * ‖a‖ := by
28   have hid : (r - T a) - (s - S a) = (r - s) - (T - S) a := by
29     simp only [sub_apply]
30     abel
31   rw [hid]
32   calc
33     ‖(r - s) - (T - S) a‖ ≤ ‖r - s‖ + ‖(T - S) a‖ := norm_sub_le _ _
34     _ ≤ δ + ‖T - S‖ * ‖a‖ := add_le_add hrs ((T - S).le_opNorm a)
35     _ ≤ δ + η * ‖a‖ := add_le_add (le_refl δ)
36       (mul_le_mul_of_nonneg_right hTS (norm_nonneg a))
37 
38 /-- The reverse triangle inequality controls the change in the residual norm. -/
39 theorem candidate_residual_abs_bound
40     (T S : H →L[ℝ] Y) (r s : Y) {η δ : ℝ}
41     (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ) (a : H) :
42     |‖r - T a‖ - ‖s - S a‖| ≤ δ + η * ‖a‖ := by
43   exact (abs_norm_sub_norm_le _ _).trans
44     (candidate_residual_difference_bound T S r s hTS hrs a)
45 
46 /-- Candidate-level uncertainty certificate, before imposing any fixed budget. -/
47 theorem candidate_residual_le
48     (T S : H →L[ℝ] Y) (r s : Y) {η δ : ℝ}
49     (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ) (a : H) :
50     ‖r - T a‖ ≤ ‖s - S a‖ + δ + η * ‖a‖ := by
51   have h := (abs_le.mp (candidate_residual_abs_bound T S r s hTS hrs a)).2
52   linarith
53 
54 /-- One common feasible ball gives the uniform candidate error allowance. -/
55 theorem budget_candidate_residual_abs_bound
56     (T S : H →L[ℝ] Y) (r s : Y) {η δ M : ℝ}
57     (hη : 0 ≤ η) (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ)
58     {a : H} (ha : ‖a‖ ≤ M) :
59     |‖r - T a‖ - ‖s - S a‖| ≤ δ + η * M := by
60   exact (candidate_residual_abs_bound T S r s hTS hrs a).trans
61     (add_le_add (le_refl δ) (mul_le_mul_of_nonneg_left ha hη))
62 
63 variable [CompleteSpace H] [CompleteSpace Y]
64 
65 /-- Evaluate the first profile at a minimizer for the second, on the same ball. -/
66 theorem beta_le_beta_add_uncertainty
67     (T S : H →L[ℝ] Y) (r s : Y) {η δ M : ℝ}
68     (hM : 0 ≤ M) (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ) :
69     BudgetProfile.beta T r M ≤ BudgetProfile.beta S s M + (δ + η * M) := by
70   have hη : 0 ≤ η := (norm_nonneg (T - S)).trans hTS
71   obtain ⟨a, ha, hamin⟩ := BudgetProfile.exists_budget_minimizer S s hM
72   have h := (abs_le.mp
73     (budget_candidate_residual_abs_bound T S r s hη hTS hrs ha)).2
74   calc
75     BudgetProfile.beta T r M ≤ ‖r - T a‖ := BudgetProfile.beta_le_residual T r ha
76     _ ≤ ‖s - S a‖ + (δ + η * M) := by linarith
77     _ = BudgetProfile.beta S s M + (δ + η * M) := by rw [hamin]
78 
79 /-- WR05: fixed-budget profiles vary by at most the explicit model/data allowance.
80 The norm bounds already force η and δ to be nonnegative. The source, target,
81 and feasible correction ball are identical in the two problems. -/
82 theorem beta_abs_sub_le
83     (T S : H →L[ℝ] Y) (r s : Y) {η δ M : ℝ}
84     (hM : 0 ≤ M) (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ) :
85     |BudgetProfile.beta T r M - BudgetProfile.beta S s M| ≤ δ + η * M := by
86   have hST : ‖S - T‖ ≤ η := by simpa only [norm_sub_rev] using hTS
87   have hsr : ‖s - r‖ ≤ δ := by simpa only [norm_sub_rev] using hrs
88   have h₁ := beta_le_beta_add_uncertainty T S r s hM hTS hrs
89   have h₂ := beta_le_beta_add_uncertainty S T s r hM hST hsr
90   exact abs_le.mpr ⟨by linarith, by linarith⟩
91 
92 /-- WR05: any nominal unit-ball dual witness gives a lower certificate for the
93 true problem after subtracting the datum and operator uncertainty allowance. -/
94 theorem nominal_dual_lower_certificate
95     (T S : H →L[ℝ] Y) (r s : Y) {η δ M : ℝ}
96     (hM : 0 ≤ M) (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ)
97     {z : Y} (hz : ‖z‖ ≤ 1) :
98     ⟪s, z⟫ - M * ‖S.adjoint z‖ - δ - η * M ≤ BudgetProfile.beta T r M := by
99   have hdual := BudgetDuality.dualValue_le_beta S s hM hz
100   have hprofile := (abs_le.mp (beta_abs_sub_le T S r s hM hTS hrs)).1
101   linarith
102 
103 /-- A strict robust nominal certificate excludes every feasible true correction. -/
104 theorem excludes_budget_of_nominal_dual_certificate
105     (T S : H →L[ℝ] Y) (r s : Y) {η δ M ε : ℝ}
106     (hM : 0 ≤ M) (hTS : ‖T - S‖ ≤ η) (hrs : ‖r - s‖ ≤ δ)
107     {z : Y} (hz : ‖z‖ ≤ 1)
108     (hcert : ε < ⟪s, z⟫ - M * ‖S.adjoint z‖ - δ - η * M)
109     {a : H} (ha : ‖a‖ ≤ M) : ε < ‖r - T a‖ := by
110   exact hcert.trans_le ((nominal_dual_lower_certificate T S r s hM hTS hrs hz).trans
111     (BudgetProfile.beta_le_residual T r ha))
112 
113 end KomorebiSpace.BudgetRobustness

Back to source controls