QuantitativeDescent.lean

1 import KomorebiSpace.HilbertKernelProjection
2 import Mathlib.Analysis.InnerProductSpace.Basic
3 import Mathlib.Tactic.Linarith
4 import Mathlib.Tactic.Ring
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Quantitative descent through the locally exact subspace
10 
11 D is the local defect, C the overlap defect. The second-stage operator is C
12 restricted to ker D, not the unrestricted C. The two-stage projection is proved
13 to equal the existing orthogonal projection for the joint defect. All constants
14 refer to declared norms. No stability of the restricted operator is implicit.
15 -/
16 universe u v w
17 noncomputable section
18 namespace KomorebiSpace
19 namespace QuantitativeDescent
20 open HilbertKernelProjection
21 variable {E : Type u} {R : Type v} {Y : Type w}
22 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
23 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
24 variable [NormedAddCommGroup Y] [NormedSpace ℝ Y]
25 variable (D : E →L[ℝ] R) (C : E →L[ℝ] Y)
26 
27 /-- Combined local and overlap defect; its target has the product maximum norm. -/
28 def joint : E →L[ℝ] R × Y := D.prod C
29 
30 omit [CompleteSpace E] in
31 @[simp] theorem joint_apply (x : E) : joint D C x = (D x, C x) := rfl
32 
33 omit [CompleteSpace E] in
34 @[simp] theorem joint_zero_iff (x : E) : joint D C x = 0 ↔ D x = 0 ∧ C x = 0 := by
35   change (D x, C x) = (0, 0) ↔ _
36   simp only [Prod.mk.injEq]
37 
38 /-- Overlap matching is performed inside the already locally exact space. -/
39 def matching : D.ker →L[ℝ] Y := C.comp D.ker.subtypeL
40 
41 omit [CompleteSpace E] in
42 @[simp] theorem matching_apply (x : D.ker) : matching D C x = C x.val := rfl
43 
44 /-- The first-stage projection retains its proof of local exactness. -/
45 def locallyExact : E →L[ℝ] D.ker := D.ker.orthogonalProjectionOnto
46 
47 @[simp] theorem locallyExact_val (x : E) :
48     (locallyExact D x).val = projection D x := rfl
49 
50 /-- The second projection remains inside ker D. -/
51 def repair : E →L[ℝ] E :=
52   D.ker.subtypeL.comp ((projection (matching D C)).comp (locallyExact D))
53 
54 @[simp] theorem repair_local (x : E) : D (repair D C x) = 0 :=
55   (projection (matching D C) (locallyExact D x)).property
56 
57 @[simp] theorem repair_overlap (x : E) : C (repair D C x) = 0 :=
58   projection_exact (matching D C) (locallyExact D x)
59 
60 /-- The two-stage construction equals the canonical joint-kernel projection. -/
61 theorem repair_eq_projection (x : E) : repair D C x = projection (joint D C) x := by
62   symm
63   apply projection_unique
64   · exact (joint_zero_iff D C _).mpr ⟨repair_local D C x, repair_overlap D C x⟩
65   · intro y hy
66     have hy' := (joint_zero_iff D C y).mp hy
67     have h₁ := error_orthogonal D x y hy'.1
68     have h₂ := error_orthogonal (matching D C) (locallyExact D x) ⟨y, hy'.1⟩ hy'.2
69     change inner ℝ y (projection D x - repair D C x) = 0 at h₂
70     change inner ℝ y (x - repair D C x) = 0
71     rw [show x - repair D C x = (x - projection D x) +
72       (projection D x - repair D C x) by abel, inner_add_right, h₁, h₂, add_zero]
73 
74 @[simp] theorem repair_fixes (x : E) (hD : D x = 0) (hC : C x = 0) :
75     repair D C x = x := by
76   rw [repair_eq_projection]
77   exact projection_fixes _ _ ((joint_zero_iff D C x).mpr ⟨hD, hC⟩)
78 
79 @[simp] theorem repair_idempotent (x : E) : repair D C (repair D C x) = repair D C x :=
80   repair_fixes D C _ (repair_local D C x) (repair_overlap D C x)
81 
82 theorem repair_norm (x : E) : ‖repair D C x‖ ≤ ‖x‖ := by
83   rw [repair_eq_projection]
84   exact projection_norm _ _
85 
86 theorem repair_best (x y : E) (hD : D y = 0) (hC : C y = 0) :
87     ‖x - repair D C x‖ ≤ ‖x-y‖ := by
88   rw [repair_eq_projection]
89   exact projection_best _ _ _ ((joint_zero_iff D C y).mpr ⟨hD, hC⟩)
90 
91 /-- Exact Pythagorean distance to any other globally coherent candidate. -/
92 theorem distance_squared (x y : E) (hD : D y=0) (hC : C y=0) :
93     ‖x-y‖^2=‖x-repair D C x‖^2+‖repair D C x-y‖^2 := by
94   have he : inner ℝ (x-repair D C x) (repair D C x-y)=0 := by
95     rw [real_inner_comm, repair_eq_projection]
96     apply error_orthogonal (joint D C) x
97     change joint D C (projection (joint D C) x-y)=0
98     rw [map_sub, projection_exact, (joint_zero_iff D C y).mpr ⟨hD,hC⟩,sub_self]
99   rw [show x-y=(x-repair D C x)+(repair D C x-y) by abel,
100     norm_add_sq_real,he,mul_zero,add_zero]
101 
102 /-- The constructed global repair is the unique nearest joint-exact candidate. -/
103 theorem nearest_unique (x y : E) (hD : D y=0) (hC : C y=0)
104     (hnear : ‖x-y‖ ≤ ‖x-repair D C x‖) : y=repair D C x := by
105   have he := distance_squared D C x y hD hC
106   have hsq : ‖repair D C x-y‖^2=0 := by
107     nlinarith [norm_nonneg (x-y),norm_nonneg (x-repair D C x),
108       sq_nonneg ‖repair D C x-y‖]
109   have hn : ‖repair D C x-y‖=0 := by nlinarith [norm_nonneg (repair D C x-y)]
110   exact (sub_eq_zero.mp (norm_eq_zero.mp hn)).symm
111 
112 /-- Exact orthogonality of local error and the subsequent matching correction. -/
113 theorem errors_orthogonal (x : E) :
114     inner ℝ (x - projection D x) (projection D x - repair D C x) = 0 := by
115   rw [real_inner_comm]
116   apply error_orthogonal D x
117   change D (projection D x - repair D C x) = 0
118   rw [map_sub, projection_exact, repair_local, sub_self]
119 
120 /-- Pythagoras separates local correction from restricted overlap correction. -/
121 theorem error_squared (x : E) :
122     ‖x-repair D C x‖^2 = ‖x-projection D x‖^2 +
123       ‖projection D x-repair D C x‖^2 := by
124   rw [show x-repair D C x = (x-projection D x) +
125     (projection D x-repair D C x) by abel]
126   rw [norm_add_sq_real, errors_orthogonal, mul_zero, add_zero]
127 
128 /-- A norm bound on C only in directions removed by the first projection. -/
129 def InteractionBound (γ : ℝ) : Prop :=
130   ∀ u : E, u ∈ D.kerᗮ → ‖C u‖ ≤ γ * ‖u‖
131 
132 omit [CompleteSpace E] in
133 theorem operator_interaction : InteractionBound D C ‖C‖ := by
134   intro u _
135   exact C.le_opNorm u
136 
137 theorem matching_input_bound {a γ : ℝ}
138     (hlocal : ∀ x, ‖x-projection D x‖ ≤ a*‖D x‖)
139     (hγ : 0 ≤ γ) (hint : InteractionBound D C γ) (x : E) :
140     ‖matching D C (locallyExact D x)‖ ≤ ‖C x‖ + γ*a*‖D x‖ := by
141   change ‖C (projection D x)‖ ≤ _
142   calc
143     _ = ‖C x - C (x-projection D x)‖ := by rw [map_sub]; congr 1; abel
144     _ ≤ ‖C x‖ + ‖C (x-projection D x)‖ := norm_sub_le _ _
145     _ ≤ ‖C x‖ + γ*‖x-projection D x‖ :=
146       add_le_add le_rfl (hint _ (error_orthogonal D x))
147     _ ≤ _ := by
148       have h := mul_le_mul_of_nonneg_left (hlocal x) hγ
149       nlinarith
150 
151 /-- Two distinct measured defects control the actual global correction. -/
152 theorem repair_error {a b γ : ℝ} (hb : 0 ≤ b) (hγ : 0 ≤ γ)
153     (hlocal : ∀ x, ‖x-projection D x‖ ≤ a*‖D x‖)
154     (hmatch : ∀ z, ‖z-projection (matching D C) z‖ ≤ b*‖matching D C z‖)
155     (hint : InteractionBound D C γ) (x : E) :
156     ‖x-repair D C x‖ ≤ a*(1+b*γ)*‖D x‖ + b*‖C x‖ := by
157   have h₂ := hmatch (locallyExact D x)
158   change ‖projection D x-repair D C x‖ ≤ b*‖matching D C (locallyExact D x)‖ at h₂
159   have h₃ := mul_le_mul_of_nonneg_left
160     (matching_input_bound D C hlocal hγ hint x) hb
161   have ht := norm_sub_le_norm_sub_add_norm_sub x (projection D x) (repair D C x)
162   nlinarith [hlocal x]
163 
164 /-- Sharper squared bound from the orthogonal two-stage decomposition. -/
165 theorem repair_error_squared {a b γ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hγ : 0 ≤ γ)
166     (hlocal : ∀ x, ‖x-projection D x‖ ≤ a*‖D x‖)
167     (hmatch : ∀ z, ‖z-projection (matching D C) z‖ ≤ b*‖matching D C z‖)
168     (hint : InteractionBound D C γ) (x : E) :
169     ‖x-repair D C x‖^2 ≤ (a*‖D x‖)^2 +
170       (b*(‖C x‖+γ*a*‖D x‖))^2 := by
171   have h₁ := hlocal x
172   have h₂ := (hmatch (locallyExact D x)).trans
173     (mul_le_mul_of_nonneg_left (matching_input_bound D C hlocal hγ hint x) hb)
174   change ‖projection D x-repair D C x‖ ≤ b*(‖C x‖+γ*a*‖D x‖) at h₂
175   rw [error_squared]
176   have hn₁ := norm_nonneg (x-projection D x)
177   have hn₂ := norm_nonneg (projection D x-repair D C x)
178   have hn₃ : 0 ≤ a*‖D x‖ := mul_nonneg ha (norm_nonneg _)
179   nlinarith [sq_nonneg (a*‖D x‖-‖x-projection D x‖),
180     sq_nonneg (b*(‖C x‖+γ*a*‖D x‖)-‖projection D x-repair D C x‖)]
181 
182 end QuantitativeDescent
183 end KomorebiSpace
184 end

Back to source controls