RegularizationCertificates.lean

1 import KomorebiSpace.RegularizedHilbertRepair
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Independent primal/dual certificates and inexact correction bounds
7 
8 The dual witness is arbitrary. Its gap is checked by an exact sum-of-squares
9 identity. A proposed correction need not solve the normal equation. Every
10 bound refers to the declared positive parameter and the actual Hilbert norm.
11 -/
12 noncomputable section
13 universe u v
14 namespace KomorebiSpace.RegularizationCertificates
15 open scoped RealInnerProductSpace
16 open RegularizedHilbertRepair
17 variable {H : Type u} {Y : Type v}
18 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
19 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
20 variable (T : H →L[ℝ] Y) (α : ℝ)
21 
22 def dual (r z : Y) : ℝ := 2*⟪r,z⟫ - ‖z‖^2 - ‖T.adjoint z‖^2/α
23 
24 /-- A certificate for all primal vectors, not a test against a finite sample. -/
25 theorem primal_dual_gap (hα : 0 < α) (r z : Y) (a : H) :
26     objective T α r a - dual T α r z =
27       ‖T a-r+z‖^2 + ‖T.adjoint z-α • a‖^2/α := by
28   simp only [objective, dual, norm_add_sq_real, norm_sub_sq_real,
29     inner_sub_left, real_inner_smul_right, ContinuousLinearMap.adjoint_inner_left, map_smul,
30     norm_smul, Real.norm_eq_abs, abs_of_pos hα]
31   rw [real_inner_comm z (T a)]
32   field_simp
33   ring
34 
35 theorem dual_le_objective (hα : 0 < α) (r z : Y) (a : H) :
36     dual T α r z ≤ objective T α r a := by
37   have he := primal_dual_gap T α hα r z a
38   have hn := div_nonneg (sq_nonneg ‖T.adjoint z-α • a‖) hα.le
39   nlinarith [sq_nonneg ‖T a-r+z‖]
40 
41 /-- The residual is a natural dual witness even when the proposed solver is inexact. -/
42 theorem residual_witness_gap (hα : 0 < α) (r : Y) (a : H) :
43     objective T α r a - dual T α r (r-T a) = ‖gradient T α r a‖^2/α := by
44   rw [primal_dual_gap T α hα]
45   have h1 : T a-r+(r-T a) = 0 := by abel
46   have h2 : T.adjoint (r-T a)-α • a = -gradient T α r a := by
47     rw [gradient, normal_apply, map_sub]
48     abel
49   rw [h1, h2, norm_zero, zero_pow (by decide : 2 ≠ 0), zero_add, norm_neg]
50 
51 theorem dual_at_correction (hα : 0 < α) (r : Y) :
52     dual T α r (r-T (correction T α hα r)) = objective T α r (correction T α hα r) := by
53   have he := residual_witness_gap T α hα r (correction T α hα r)
54   rw [gradient_correction, norm_zero, zero_pow (by decide : 2 ≠ 0), zero_div] at he
55   linarith
56 
57 theorem dual_maximizer (hα : 0 < α) (r z : Y) :
58     dual T α r z ≤ dual T α r (r-T (correction T α hα r)) := by
59   rw [dual_at_correction]
60   exact dual_le_objective T α hα r z _
61 
62 theorem gap_controls_correction (hα : 0 < α) (r z : Y) (a : H) :
63     α*‖a-correction T α hα r‖^2 ≤ objective T α r a - dual T α r z := by
64   have he := energy_identity T α hα r a
65   have hd := dual_le_objective T α hα r z (correction T α hα r)
66   nlinarith [sq_nonneg ‖T (a-correction T α hα r)‖]
67 
68 /-- A unit support witness is a lower bound against the entire correction ball. -/
69 theorem budget_witness_bound (r z : Y) (a : H) (M : ℝ)
70     (hz : ‖z‖ ≤ 1) (ha : ‖a‖ ≤ M) :
71     ⟪r,z⟫-M*‖T.adjoint z‖ ≤ ‖r-T a‖ := by
72   have h1 := real_inner_le_norm (r-T a) z
73   have h2 := real_inner_le_norm a (T.adjoint z)
74   rw [ContinuousLinearMap.adjoint_inner_right] at h2
75   have h3 := mul_le_mul_of_nonneg_left hz (norm_nonneg (r-T a))
76   have h4 := mul_le_mul_of_nonneg_right ha (norm_nonneg (T.adjoint z))
77   rw [inner_sub_left] at h1
78   nlinarith
79 
80 /-- The exact normal equation gives the supporting equality before normalization. -/
81 theorem budget_support_identity (hα : 0 < α) (r : Y) :
82     ⟪r,r-T (correction T α hα r)⟫ - ‖correction T α hα r‖ *
83       ‖T.adjoint (r-T (correction T α hα r))‖ =
84       ‖r-T (correction T α hα r)‖^2 := by
85   have hn := normal_equation T α hα r
86   have hi := congrArg (fun z => ⟪correction T α hα r,z⟫) hn
87   rw [ContinuousLinearMap.adjoint_inner_right, real_inner_smul_right,
88     real_inner_self_eq_norm_sq] at hi
89   have he := real_inner_self_eq_norm_sq (r-T (correction T α hα r))
90   rw [inner_sub_left] at he
91   rw [hn, norm_smul, Real.norm_eq_abs, abs_of_pos hα]
92   nlinarith
93 
94 def unitResidual (hα : 0 < α) (r : Y) : Y :=
95   ‖r-T (correction T α hα r)‖⁻¹ • (r-T (correction T α hα r))
96 
97 theorem unitResidual_norm (hα : 0 < α) (r : Y)
98     (hv : r-T (correction T α hα r) ≠ 0) : ‖unitResidual T α hα r‖ = 1 := by
99   simp only [unitResidual, norm_smul, Real.norm_eq_abs, abs_inv, abs_norm]
100   exact inv_mul_cancel₀ (norm_ne_zero_iff.mpr hv)
101 
102 theorem unitResidual_support (hα : 0 < α) (r : Y)
103     (hv : r-T (correction T α hα r) ≠ 0) :
104     ⟪r,unitResidual T α hα r⟫ - ‖correction T α hα r‖ *
105       ‖T.adjoint (unitResidual T α hα r)‖ = ‖r-T (correction T α hα r)‖ := by
106   have hs := budget_support_identity T α hα r
107   have hn : ‖r-T (correction T α hα r)‖ ≠ 0 := norm_ne_zero_iff.mpr hv
108   simp only [unitResidual, real_inner_smul_right, map_smul,
109     norm_smul, Real.norm_eq_abs, abs_inv, abs_norm]
110   calc
111     ‖r-T (correction T α hα r)‖⁻¹ * ⟪r,r-T (correction T α hα r)⟫ -
112         ‖correction T α hα r‖ * (‖r-T (correction T α hα r)‖⁻¹ *
113           ‖T.adjoint (r-T (correction T α hα r))‖) =
114       ‖r-T (correction T α hα r)‖⁻¹ *
115         (⟪r,r-T (correction T α hα r)⟫ - ‖correction T α hα r‖ *
116           ‖T.adjoint (r-T (correction T α hα r))‖) := by ring
117     _ = ‖r-T (correction T α hα r)‖⁻¹ * ‖r-T (correction T α hα r)‖^2 := by rw [hs]
118     _ = ‖r-T (correction T α hα r)‖ := by field_simp
119 
120 end KomorebiSpace.RegularizationCertificates

Back to source controls