ProtectedRegularizedRepair.lean

1 import KomorebiSpace.RegularizationCertificates
2 import KomorebiSpace.ProtectedHilbertRepair
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Regularization on the actual protected Hilbert kernel
8 
9 This is a bridge to ProtectedHilbertRepair.restricted, not a replacement
10 notion of protected correction. Measured residual data are independent of
11 D f. Protection holds for every such datum, but measured fit is not silently
12 identified with the actual residual of the repaired candidate.
13 -/
14 noncomputable section
15 universe u v w
16 namespace KomorebiSpace.ProtectedRegularizedRepair
17 open scoped RealInnerProductSpace
18 open ProtectedHilbertRepair
19 variable {E : Type u} {Y : Type v} {S : Type w}
20 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
21 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
22 variable [NormedAddCommGroup S] [NormedSpace ℝ S]
23 variable (D : E →L[ℝ] Y) (p : E →L[ℝ] S) (α : ℝ)
24 
25 /-- The restricted adjoint is the ambient adjoint projected into the permitted kernel. -/
26 theorem restricted_adjoint (r : Y) :
27     (restricted D p).adjoint r = p.ker.orthogonalProjectionOnto (D.adjoint r) := by
28   simp [restricted, ContinuousLinearMap.adjoint_comp, Submodule.adjoint_subtypeL]
29 
30 def correction (hα : 0 < α) (r : Y) : p.ker :=
31   RegularizedHilbertRepair.correction (restricted D p) α hα r
32 
33 def repair (hα : 0 < α) (f : E) (r : Y) : E := f-(correction D p α hα r).val
34 
35 theorem correction_permitted (hα : 0 < α) (r : Y) :
36     p (correction D p α hα r).val = 0 := (correction D p α hα r).property
37 
38 theorem repair_preserves (hα : 0 < α) (f : E) (r : Y) :
39     p (repair D p α hα f r) = p f := by
40   rw [repair, map_sub, correction_permitted, sub_zero]
41 
42 theorem actual_residual (hα : 0 < α) (f : E) (r : Y) :
43     D (repair D p α hα f r) = D f-restricted D p (correction D p α hα r) := by
44   rw [repair, map_sub]
45   rfl
46 
47 theorem projected_normal_equation (hα : 0 < α) (r : Y) :
48     p.ker.orthogonalProjectionOnto (D.adjoint (r-D (correction D p α hα r).val)) =
49       α • correction D p α hα r := by
50   rw [← restricted_adjoint]
51   exact RegularizedHilbertRepair.normal_equation (restricted D p) α hα r
52 
53 theorem energy_identity (hα : 0 < α) (r : Y) (a : p.ker) :
54     (‖D a.val-r‖^2+α*‖a‖^2) -
55       (‖D (correction D p α hα r).val-r‖^2+α*‖correction D p α hα r‖^2) =
56       ‖D (a-correction D p α hα r).val‖^2 + α*‖a-correction D p α hα r‖^2 :=
57   RegularizedHilbertRepair.energy_identity (restricted D p) α hα r a
58 
59 theorem unique_best (hα : 0 < α) (r : Y) :
60     ∃! a : p.ker, ∀ b : p.ker,
61       ‖D a.val-r‖^2+α*‖a‖^2 ≤ ‖D b.val-r‖^2+α*‖b‖^2 :=
62   RegularizedHilbertRepair.exists_unique_minimizer (restricted D p) α hα r
63 
64 omit [CompleteSpace E] in
65 /-- An inexact proposal remains exactly protected when it is in the actual subtype. -/
66 theorem proposal_preserves (f : E) (a : p.ker) : p (f-a.val) = p f := by
67   have ha : p a.val = 0 := a.property
68   rw [map_sub, ha, sub_zero]
69 
70 theorem proposal_error (hα : 0 < α) (f : E) (r : Y) (a : p.ker) :
71     ‖(f-a.val)-repair D p α hα f r‖ ≤
72       ‖RegularizedHilbertRepair.gradient (restricted D p) α r a‖/α := by
73   have he : (f-a.val)-repair D p α hα f r = (correction D p α hα r).val-a.val := by
74     rw [repair]; abel
75   rw [he, norm_sub_rev]
76   exact RegularizedHilbertRepair.correction_error_bound (restricted D p) α hα r a
77 
78 theorem proposal_dual_gap (hα : 0 < α) (r z : Y) (a : p.ker) :
79     RegularizedHilbertRepair.objective (restricted D p) α r a -
80       RegularizationCertificates.dual (restricted D p) α r z =
81       ‖D a.val-r+z‖^2 +
82         ‖p.ker.orthogonalProjectionOnto (D.adjoint z)-α • a‖^2/α := by
83   rw [RegularizationCertificates.primal_dual_gap _ _ hα, restricted_adjoint]
84   rfl
85 
86 end KomorebiSpace.ProtectedRegularizedRepair

Back to source controls