BudgetDuality.lean

1 import KomorebiSpace.BudgetProfile
2 import Mathlib.Analysis.InnerProductSpace.Adjoint
3 import Mathlib.Analysis.InnerProductSpace.Projection.Minimal
4 import Mathlib.Topology.MetricSpace.HausdorffDistance
5 import Mathlib.Tactic.FieldSimp
6 import Mathlib.Tactic.Linarith
7 import Mathlib.Tactic.Ring
8 
9 set_option autoImplicit false
10 
11 noncomputable section
12 universe u v
13 namespace KomorebiSpace.BudgetDuality
14 open scoped RealInnerProductSpace
15 variable {H : Type u} {Y : Type v}
16 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
17 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
18 
19 /-- Every admissible dual vector bounds every candidate in the fixed correction ball. -/
20 theorem dualValue_le_residual (T : H →L[ℝ] Y) (r : Y) {M : ℝ}
21     {a : H} (ha : ‖a‖ ≤ M) {z : Y} (hz : ‖z‖ ≤ 1) :
22     ⟪r, z⟫ - M * ‖T.adjoint z‖ ≤ ‖r - T a‖ := by
23   have hres : ⟪r - T a, z⟫ ≤ ‖r - T a‖ := calc
24     _ ≤ ‖r - T a‖ * ‖z‖ := real_inner_le_norm _ _
25     _ ≤ ‖r - T a‖ * 1 := mul_le_mul_of_nonneg_left hz (norm_nonneg _)
26     _ = ‖r - T a‖ := mul_one _
27   have himage : ⟪T a, z⟫ ≤ M * ‖T.adjoint z‖ := calc
28     _ = ⟪a, T.adjoint z⟫ := (ContinuousLinearMap.adjoint_inner_right T a z).symm
29     _ ≤ ‖a‖ * ‖T.adjoint z‖ := real_inner_le_norm _ _
30     _ ≤ M * ‖T.adjoint z‖ := mul_le_mul_of_nonneg_right ha (norm_nonneg _)
31   rw [inner_sub_left] at hres
32   linarith
33 
34 omit [CompleteSpace H] in
35 /-- If a feasible point maximizes a linear pairing on a ball, it attains its exact support value.
36 The proof includes zero radius and zero supporting vector. -/
37 theorem ball_support_eq {M : ℝ} (hM : 0 ≤ M) (g a : H) (ha : ‖a‖ ≤ M)
38     (hmax : ∀ b : H, ‖b‖ ≤ M → ⟪b, g⟫ ≤ ⟪a, g⟫) :
39     ⟪a, g⟫ = M * ‖g‖ := by
40   by_cases hg : g = 0
41   · simp [hg]
42   have hgpos : 0 < ‖g‖ := norm_pos_iff.mpr hg
43   have hgn : ‖g‖ ≠ 0 := ne_of_gt hgpos
44   have hn : ‖(M / ‖g‖) • g‖ = M := by
45     rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (div_nonneg hM hgpos.le)]
46     exact div_mul_cancel₀ M hgn
47   have hi : ⟪(M / ‖g‖) • g, g⟫ = M * ‖g‖ := by
48     rw [real_inner_smul_left, real_inner_self_eq_norm_sq]
49     field_simp
50   apply le_antisymm
51   · exact (real_inner_le_norm a g).trans
52       (mul_le_mul_of_nonneg_right ha (norm_nonneg _))
53   · simpa only [hi] using hmax ((M / ‖g‖) • g) hn.le
54 
55 /-- A variationally minimizing residual gives an attaining dual vector.
56 This helper isolates the elementary support calculation from existence of a minimizer. -/
57 theorem exists_sharp_witness_of_variational (T : H →L[ℝ] Y) (r : Y)
58     {M : ℝ} (hM : 0 ≤ M) (a : H) (ha : ‖a‖ ≤ M)
59     (hvar : ∀ b : H, ‖b‖ ≤ M → ⟪r - T a, T b - T a⟫ ≤ 0) :
60     ∃ z : Y, ‖z‖ ≤ 1 ∧ ⟪r, z⟫ - M * ‖T.adjoint z‖ = ‖r - T a‖ := by
61   by_cases hv : r - T a = 0
62   · refine ⟨0, by simp, ?_⟩
63     simp [hv]
64   have hvpos : 0 < ‖r - T a‖ := norm_pos_iff.mpr hv
65   have hvn : ‖r - T a‖ ≠ 0 := ne_of_gt hvpos
66   let z : Y := ‖r - T a‖⁻¹ • (r - T a)
67   have hz : ‖z‖ = 1 := by
68     dsimp [z]
69     rw [norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.mpr hvpos), inv_mul_cancel₀ hvn]
70   have hmax : ∀ b : H, ‖b‖ ≤ M → ⟪b, T.adjoint z⟫ ≤ ⟪a, T.adjoint z⟫ := by
71     intro b hb
72     have hi := hvar b hb
73     rw [inner_sub_right] at hi
74     rw [ContinuousLinearMap.adjoint_inner_right, ContinuousLinearMap.adjoint_inner_right]
75     dsimp [z]
76     rw [real_inner_smul_right, real_inner_smul_right]
77     have hi' : ⟪T b, r - T a⟫ ≤ ⟪T a, r - T a⟫ := by
78       simpa only [real_inner_comm] using sub_nonpos.mp hi
79     exact mul_le_mul_of_nonneg_left hi' (inv_nonneg.mpr hvpos.le)
80   have hs := ball_support_eq hM (T.adjoint z) a ha hmax
81   have hir : ⟪r - T a, z⟫ = ‖r - T a‖ := by
82     dsimp [z]
83     rw [real_inner_smul_right, real_inner_self_eq_norm_sq]
84     field_simp
85   refine ⟨z, hz.le, ?_⟩
86   rw [← hs, ContinuousLinearMap.adjoint_inner_right, ← inner_sub_left]
87   exact hir
88 
89 /-- The universal dual bound at every nonnegative budget. -/
90 theorem dualValue_le_beta (T : H →L[ℝ] Y) (r : Y) {M : ℝ}
91     (hM : 0 ≤ M) {z : Y} (hz : ‖z‖ ≤ 1) :
92     ⟪r, z⟫ - M * ‖T.adjoint z‖ ≤ BudgetProfile.beta T r M := by
93   obtain ⟨a, ha, heq⟩ := BudgetProfile.exists_budget_minimizer T r hM
94   exact (dualValue_le_residual T r ha hz).trans_eq heq
95 
96 omit [CompleteSpace H] [CompleteSpace Y] in
97 /-- The fixed-budget minimizer satisfies the full convex variational inequality. -/
98 theorem minimizer_variational (T : H →L[ℝ] Y) (r : Y) {M : ℝ}
99     (a : H) (ha : ‖a‖ ≤ M) (hmin : ‖r - T a‖ = BudgetProfile.beta T r M) :
100     ∀ b : H, ‖b‖ ≤ M → ⟪r - T a, T b - T a⟫ ≤ 0 := by
101   have ha' : T a ∈ T '' Metric.closedBall 0 M :=
102     ⟨a, by simpa only [Metric.mem_closedBall, dist_zero_right] using ha, rfl⟩
103   have hmin' : ‖r - T a‖ = ⨅ w : (T '' Metric.closedBall 0 M), ‖r - w‖ := by
104     simpa only [BudgetProfile.beta, Metric.infDist_eq_iInf, dist_eq_norm] using hmin
105   have hv := (norm_eq_iInf_iff_real_inner_le_zero
106     (BudgetProfile.convex_budget_image T M) ha').mp hmin'
107   intro b hb
108   exact hv (T b) ⟨b, by simpa only [Metric.mem_closedBall, dist_zero_right] using hb, rfl⟩
109 
110 /-- WR04 sharpness: a witness in the closed unit ball attains the exact budget profile.
111 No closed-range, finite-dimensionality, positive-budget, or nonzero-residual assumption is needed. -/
112 theorem exists_attaining_dual_witness (T : H →L[ℝ] Y) (r : Y) {M : ℝ}
113     (hM : 0 ≤ M) : ∃ z : Y, ‖z‖ ≤ 1 ∧
114     ⟪r, z⟫ - M * ‖T.adjoint z‖ = BudgetProfile.beta T r M := by
115   obtain ⟨a, ha, heq⟩ := BudgetProfile.exists_budget_minimizer T r hM
116   obtain ⟨z, hz, hvalue⟩ := exists_sharp_witness_of_variational T r hM a ha
117     (minimizer_variational T r a ha heq)
118   exact ⟨z, hz, hvalue.trans heq⟩
119 
120 /-- WR04 as a literal maximum, combining existence with the universal upper bound. -/
121 theorem sharp_budget_duality (T : H →L[ℝ] Y) (r : Y) {M : ℝ}
122     (hM : 0 ≤ M) :
123     IsGreatest ((fun z : Y => ⟪r, z⟫ - M * ‖T.adjoint z‖) ''
124       Metric.closedBall (0 : Y) 1) (BudgetProfile.beta T r M) := by
125   obtain ⟨z, hz, heq⟩ := exists_attaining_dual_witness T r hM
126   constructor
127   · exact ⟨z, by simpa only [Metric.mem_closedBall, dist_zero_right] using hz, heq⟩
128   · rintro _ ⟨w, hw, rfl⟩
129     exact dualValue_le_beta T r hM (by
130       simpa only [Metric.mem_closedBall, dist_zero_right] using hw)
131 
132 /-- Any witness above epsilon excludes every correction with that budget and residual tolerance. -/
133 theorem strict_exclusion_certificate (T : H →L[ℝ] Y) (r : Y) {M ε : ℝ}
134     {z : Y} (hz : ‖z‖ ≤ 1) (hcert : ε < ⟪r, z⟫ - M * ‖T.adjoint z‖) :
135     ¬ ∃ a : H, ‖a‖ ≤ M ∧ ‖r - T a‖ ≤ ε := by
136   rintro ⟨a, ha, hres⟩
137   exact (not_lt_of_ge ((dualValue_le_residual T r ha hz).trans hres)) hcert
138 
139 end KomorebiSpace.BudgetDuality

Back to source controls