BudgetProfileGeometry.lean

1 import KomorebiSpace.BudgetProfile
2 
3 /-!
4 # Shape of the attained budget profile (WR03)
5 
6 These statements use the actual norm on the correction space. They require no
7 finite-dimensionality, injectivity, or closed-range assumption. The zero-budget
8 case is included explicitly in the profile estimate.
9 -/
10 
11 noncomputable section
12 
13 namespace KomorebiSpace.BudgetProfileGeometry
14 
15 open KomorebiSpace.BudgetProfile
16 
17 variable {H Y : Type*}
18 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
19 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
20 
21 /-- Increasing a nonnegative correction budget cannot increase the best residual. -/
22 theorem beta_antitone (T : H →L[ℝ] Y) (r : Y) {M₁ M₂ : ℝ}
23     (h₁ : 0 ≤ M₁) (h₁₂ : M₁ ≤ M₂) : beta T r M₂ ≤ beta T r M₁ := by
24   obtain ⟨a, ha, hopt⟩ := exists_budget_minimizer T r h₁
25   exact (beta_le_residual T r (ha.trans h₁₂)).trans_eq hopt
26 
27 /-- The zero ball contains only zero, so the initial budget profile is the data norm. -/
28 theorem beta_zero (T : H →L[ℝ] Y) (r : Y) : beta T r 0 = ‖r‖ := by
29   obtain ⟨a, ha, hopt⟩ := exists_budget_minimizer T r (le_refl 0)
30   have hz : a = 0 := norm_eq_zero.mp (le_antisymm ha (norm_nonneg a))
31   simpa only [hz, map_zero, sub_zero] using hopt.symm
32 
33 /-- The exact convexity inequality, including both endpoints and zero budgets. -/
34 theorem beta_convex_combination (T : H →L[ℝ] Y) (r : Y) {M₁ M₂ t : ℝ}
35     (h₁ : 0 ≤ M₁) (h₂ : 0 ≤ M₂) (ht : 0 ≤ t) (ht₁ : t ≤ 1) :
36     beta T r (t * M₁ + (1 - t) * M₂) ≤
37       t * beta T r M₁ + (1 - t) * beta T r M₂ := by
38   obtain ⟨a₁, ha₁, heq₁⟩ := exists_budget_minimizer T r h₁
39   obtain ⟨a₂, ha₂, heq₂⟩ := exists_budget_minimizer T r h₂
40   have hs : 0 ≤ 1 - t := sub_nonneg.mpr ht₁
41   have hfeas : ‖t • a₁ + (1 - t) • a₂‖ ≤ t * M₁ + (1 - t) * M₂ := by
42     calc
43       _ ≤ ‖t • a₁‖ + ‖(1 - t) • a₂‖ := norm_add_le _ _
44       _ = t * ‖a₁‖ + (1 - t) * ‖a₂‖ := by
45         simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht, abs_of_nonneg hs]
46       _ ≤ _ := add_le_add (mul_le_mul_of_nonneg_left ha₁ ht)
47         (mul_le_mul_of_nonneg_left ha₂ hs)
48   calc
49     _ ≤ ‖r - T (t • a₁ + (1 - t) • a₂)‖ := beta_le_residual T r hfeas
50     _ = ‖t • (r - T a₁) + (1 - t) • (r - T a₂)‖ := by
51       congr 1
52       simp only [map_add, map_smul]
53       module
54     _ ≤ ‖t • (r - T a₁)‖ + ‖(1 - t) • (r - T a₂)‖ := norm_add_le _ _
55     _ = _ := by
56       simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht, abs_of_nonneg hs,
57         heq₁, heq₂]
58 
59 omit [CompleteSpace H] in
60 /-- Radially shrink any feasible vector from a positive budget to a smaller one. -/
61 theorem radial_shrink_bounds {a : H} {M₁ M₂ : ℝ}
62     (h₁ : 0 ≤ M₁) (h₂ : 0 < M₂) (h₁₂ : M₁ ≤ M₂) (ha : ‖a‖ ≤ M₂) :
63     ‖(M₁ / M₂) • a‖ ≤ M₁ ∧ ‖a - (M₁ / M₂) • a‖ ≤ M₂ - M₁ := by
64   have ht : 0 ≤ M₁ / M₂ := div_nonneg h₁ h₂.le
65   have ht₁ : M₁ / M₂ ≤ 1 := (div_le_one h₂).mpr h₁₂
66   have hprod : (M₁ / M₂) * M₂ = M₁ := div_mul_cancel₀ M₁ (ne_of_gt h₂)
67   constructor
68   · calc
69       _ = (M₁ / M₂) * ‖a‖ := by
70         simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
71       _ ≤ (M₁ / M₂) * M₂ := mul_le_mul_of_nonneg_left ha ht
72       _ = M₁ := hprod
73   · have heq : a - (M₁ / M₂) • a = (1 - M₁ / M₂) • a := by module
74     calc
75       _ = (1 - M₁ / M₂) * ‖a‖ := by
76         rw [heq, norm_smul, Real.norm_eq_abs, abs_of_nonneg (sub_nonneg.mpr ht₁)]
77       _ ≤ (1 - M₁ / M₂) * M₂ :=
78         mul_le_mul_of_nonneg_left ha (sub_nonneg.mpr ht₁)
79       _ = M₂ - M₁ := by nlinarith
80 
81 /-- The one-sided Lipschitz estimate handles the degenerate upper budget explicitly. -/
82 theorem beta_sub_le (T : H →L[ℝ] Y) (r : Y) {M₁ M₂ : ℝ}
83     (h₁ : 0 ≤ M₁) (h₁₂ : M₁ ≤ M₂) :
84     beta T r M₁ - beta T r M₂ ≤ ‖T‖ * (M₂ - M₁) := by
85   have h₂ : 0 ≤ M₂ := h₁.trans h₁₂
86   obtain hzero | hpos := h₂.eq_or_lt
87   · have hM₁ : M₁ = 0 := le_antisymm (h₁₂.trans_eq hzero.symm) h₁
88     simp only [hM₁, ← hzero, sub_self, mul_zero, le_refl]
89   · obtain ⟨a, ha, hopt⟩ := exists_budget_minimizer T r h₂
90     obtain ⟨hb, hdiff⟩ := radial_shrink_bounds h₁ hpos h₁₂ ha
91     have hbound : beta T r M₁ ≤ beta T r M₂ + ‖T‖ * (M₂ - M₁) := by
92       calc
93         _ ≤ ‖r - T ((M₁ / M₂) • a)‖ := beta_le_residual T r hb
94         _ = ‖(r - T a) + T (a - (M₁ / M₂) • a)‖ := by
95           congr 1
96           simp only [map_sub]
97           abel
98         _ ≤ ‖r - T a‖ + ‖T (a - (M₁ / M₂) • a)‖ := norm_add_le _ _
99         _ ≤ beta T r M₂ + ‖T‖ * ‖a - (M₁ / M₂) • a‖ := by
100           rw [hopt]
101           exact add_le_add (le_refl _) (T.le_opNorm _)
102         _ ≤ _ := add_le_add (le_refl _)
103           (mul_le_mul_of_nonneg_left hdiff (norm_nonneg T))
104     linarith
105 
106 /-- Both sides of the printed WR03 profile estimate, for every ordered nonnegative pair. -/
107 theorem beta_profile_bounds (T : H →L[ℝ] Y) (r : Y) {M₁ M₂ : ℝ}
108     (h₁ : 0 ≤ M₁) (h₁₂ : M₁ ≤ M₂) :
109     0 ≤ beta T r M₁ - beta T r M₂ ∧
110       beta T r M₁ - beta T r M₂ ≤ ‖T‖ * (M₂ - M₁) :=
111   ⟨sub_nonneg.mpr (beta_antitone T r h₁ h₁₂), beta_sub_le T r h₁ h₁₂⟩
112 
113 end KomorebiSpace.BudgetProfileGeometry

Back to source controls