InfiniteDiagonalModel.lean

1 import KomorebiSpace.DiagonalSeriesBounds
2 import KomorebiSpace.RegularizedHilbertRepair
3 import KomorebiSpace.BudgetProfile
4 import Mathlib.Analysis.InnerProductSpace.l2Space
5 import Mathlib.Tactic
6 
7 /-!
8 # The actual infinite Hilbert diagonal model
9 
10 Natural coordinate `j` denotes the printed positive integer `j + 1`.
11 All vectors below belong to mathlib's real `lp` space at exponent two.
12 -/
13 
14 set_option autoImplicit false
15 noncomputable section
16 namespace KomorebiSpace.DiagonalRegularization
17 open scoped RealInnerProductSpace
18 
19 /-- The real Hilbert space on the printed positive integer coordinates. -/
20 abbrev H : Type := lp (fun _ : ℕ => ℝ) 2
21 
22 private theorem hilbert_index_pos (j : ℕ) : 0 < index j := by
23   unfold index
24   positivity
25 
26 private theorem hilbert_index_ge_one (j : ℕ) : 1 ≤ index j := by
27   unfold index
28   have hj : (0 : ℝ) ≤ j := Nat.cast_nonneg j
29   linarith
30 
31 private theorem hilbert_denominator_pos (m j : ℕ) :
32     0 < (m : ℝ)^2 + (index j)^2 := by
33   have hj := hilbert_index_pos j
34   positivity
35 
36 private theorem hilbert_weight_norm_le (j : ℕ) : ‖wCoord j‖ ≤ 1 := by
37   rw [wCoord, norm_inv, Real.norm_eq_abs, abs_of_pos (hilbert_index_pos j)]
38   exact inv_le_one_of_one_le₀ (hilbert_index_ge_one j)
39 
40 private theorem hilbert_mem_of_sq_summable (f : ℕ → ℝ)
41     (hf : Summable (fun j => f j ^ 2)) : Memℓp f 2 := by
42   apply memℓp_gen
43   simpa only [ENNReal.toReal_ofNat, Real.rpow_two, Real.norm_eq_abs, sq_abs] using hf
44 
45 /-- Coordinate multiplication by the real weights `1/(j+1)`. -/
46 def Tlinear : H →ₗ[ℝ] H where
47   toFun u := ⟨fun j => wCoord j * u j,
48     (lp.memℓp u).mono' (fun j => by
49       rw [norm_mul]
50       exact mul_le_of_le_one_left (norm_nonneg _) (hilbert_weight_norm_le j))⟩
51   map_add' u v := by
52     apply lp.ext
53     funext j
54     change wCoord j * (u j + v j) = wCoord j * u j + wCoord j * v j
55     ring
56   map_smul' r u := by
57     apply lp.ext
58     funext j
59     change wCoord j * (r * u j) = r * (wCoord j * u j)
60     ring
61 
62 /-- The diagonal operator is bounded, with operator norm at most one. -/
63 def T : H →L[ℝ] H :=
64   Tlinear.mkContinuous 1 (by
65     intro u
66     rw [one_mul]
67     apply lp.norm_mono (by norm_num)
68     intro j
69     change ‖wCoord j * u j‖ ≤ ‖u j‖
70     rw [norm_mul]
71     exact mul_le_of_le_one_left (norm_nonneg _) (hilbert_weight_norm_le j))
72 
73 @[simp] theorem T_apply (u : H) (j : ℕ) : T u j = wCoord j * u j := rfl
74 
75 theorem T_norm_le (u : H) : ‖T u‖ ≤ ‖u‖ := by
76   apply lp.norm_mono (by norm_num)
77   intro j
78   rw [T_apply, norm_mul]
79   exact mul_le_of_le_one_left (norm_nonneg _) (hilbert_weight_norm_le j)
80 
81 theorem T_opNorm_le_one : ‖T‖ ≤ 1 := by
82   apply T.opNorm_le_bound (by norm_num)
83   intro u
84   simpa only [one_mul] using T_norm_le u
85 
86 /-- Self-adjointness is proved from the infinite Hilbert inner product. -/
87 theorem T_adjoint : T.adjoint = T := by
88   apply ContinuousLinearMap.ext
89   intro x
90   apply ext_inner_right ℝ
91   intro y
92   rw [ContinuousLinearMap.adjoint_inner_left, lp.inner_eq_tsum, lp.inner_eq_tsum]
93   apply tsum_congr
94   intro j
95   simp only [T_apply, Real.inner_apply]
96   ring
97 
98 theorem T_isSelfAdjoint : IsSelfAdjoint T :=
99   ContinuousLinearMap.isSelfAdjoint_iff'.mpr T_adjoint
100 
101 /-- No nonzero coordinate is killed by `T`. -/
102 theorem T_injective : Function.Injective T := by
103   intro x y h
104   apply lp.ext
105   funext j
106   have hj := congrArg (fun u : H => u j) h
107   simp only [T_apply] at hj
108   exact mul_left_cancel₀ (inv_ne_zero (ne_of_gt (hilbert_index_pos j))) hj
109 
110 /-- The escaping datum `w_j = 1/(j+1)` is square summable. -/
111 def w : H := ⟨wCoord, hilbert_mem_of_sq_summable _ summable_wCoord_sq⟩
112 
113 /-- The exact candidate regularized correction. -/
114 def a (m : ℕ) : H := ⟨aCoord m, hilbert_mem_of_sq_summable _ (summable_aCoord_sq m)⟩
115 
116 /-- The residual family in the actual Hilbert space. -/
117 def v (m : ℕ) : H := ⟨vCoord m, hilbert_mem_of_sq_summable _ (summable_vCoord_sq m)⟩
118 
119 /-- The attainable datum `b_j = 1/(j+1)^2`. -/
120 def b : H := T w
121 
122 /-- Candidate regularized correction for the attainable datum. -/
123 def c (m : ℕ) : H := T (a m)
124 
125 @[simp] theorem w_apply (j : ℕ) : w j = wCoord j := rfl
126 @[simp] theorem a_apply (m j : ℕ) : a m j = aCoord m j := rfl
127 @[simp] theorem v_apply (m j : ℕ) : v m j = vCoord m j := rfl
128 
129 @[simp] theorem b_apply (j : ℕ) : b j = bCoord j := by
130   change wCoord j * wCoord j = bCoord j
131   simp [wCoord, bCoord, pow_two, mul_inv_rev]
132 
133 @[simp] theorem c_apply (m j : ℕ) : c m j = cCoord m j := by
134   change wCoord j * aCoord m j = cCoord m j
135   unfold wCoord aCoord cCoord
136   simp only [div_eq_mul_inv, mul_inv_rev]
137   ring
138 
139 /-- The regularization parameter is exactly the inverse square of the integer. -/
140 def alpha (m : ℕ) : ℝ := ((m : ℝ)^2)⁻¹
141 
142 theorem alpha_pos {m : ℕ} (hm : 1 ≤ m) : 0 < alpha m := by
143   have hmp : 0 < (m : ℝ) := by exact_mod_cast (show 0 < m by omega)
144   unfold alpha
145   positivity
146 
147 private theorem hilbert_a_normal_coord {m : ℕ} (hm : 1 ≤ m) (j : ℕ) :
148     wCoord j * (wCoord j * aCoord m j) + alpha m * aCoord m j =
149       wCoord j * wCoord j := by
150   have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
151   have hj0 := ne_of_gt (hilbert_index_pos j)
152   have hd0 := ne_of_gt (hilbert_denominator_pos m j)
153   unfold wCoord aCoord alpha
154   field_simp [hm0, hj0, hd0]
155 
156 /-- The coordinate candidate solves the universal normal equation. -/
157 theorem a_normal {m : ℕ} (hm : 1 ≤ m) :
158     RegularizedHilbertRepair.normal T (alpha m) (a m) = T.adjoint w := by
159   rw [RegularizedHilbertRepair.normal_apply, T_adjoint]
160   apply lp.ext
161   funext j
162   change wCoord j * (wCoord j * aCoord m j) + alpha m * aCoord m j =
163     wCoord j * wCoord j
164   exact hilbert_a_normal_coord hm j
165 
166 /-- Equality with the universal unique regularized correction. -/
167 theorem a_eq_correction {m : ℕ} (hm : 1 ≤ m) :
168     a m = RegularizedHilbertRepair.correction T (alpha m) (alpha_pos hm) w :=
169   RegularizedHilbertRepair.normal_unique T (alpha m) (alpha_pos hm) w (a m) (a_normal hm)
170 
171 /-- The actual infinite residual has the printed coordinates. -/
172 theorem residual_eq_v (m : ℕ) : w - T (a m) = v m := by
173   apply lp.ext
174   funext j
175   change wCoord j - wCoord j * aCoord m j = vCoord m j
176   have hj0 := ne_of_gt (hilbert_index_pos j)
177   have hd0 := ne_of_gt (hilbert_denominator_pos m j)
178   unfold wCoord aCoord vCoord
179   field_simp [hj0, hd0]
180   ring
181 
182 /-- The Hilbert norm is the actual infinite sum, not a finite-prefix surrogate. -/
183 theorem norm_sq_eq_tsum (x : H) : ‖x‖^2 = ∑' j, (x j)^2 := by
184   rw [← real_inner_self_eq_norm_sq, lp.inner_eq_tsum]
185   apply tsum_congr
186   intro j
187   simp only [Real.inner_apply, pow_two]
188 
189 theorem norm_a_sq (m : ℕ) : ‖a m‖^2 = A m := by
190   rw [norm_sq_eq_tsum]
191   rfl
192 
193 theorem norm_v_sq (m : ℕ) : ‖v m‖^2 = B m := by
194   rw [norm_sq_eq_tsum]
195   rfl
196 
197 theorem norm_residual_sq (m : ℕ) : ‖w - T (a m)‖^2 = B m := by
198   rw [residual_eq_v, norm_v_sq]
199 
200 @[simp] theorem T_w_eq_b : T w = b := rfl
201 
202 /-- The attainable datum has the unique preimage `w`. -/
203 theorem b_preimage_unique (x : H) (hx : T x = b) : x = w :=
204   T_injective hx
205 
206 /-- In particular, `w` is a minimum-norm preimage of `b`. -/
207 theorem w_minimum_norm_preimage (x : H) (hx : T x = b) : ‖w‖ ≤ ‖x‖ := by
208   rw [b_preimage_unique x hx]
209 
210 /-- Commutativity of the actual diagonal operators transports the normal equation. -/
211 theorem c_normal {m : ℕ} (hm : 1 ≤ m) :
212     RegularizedHilbertRepair.normal T (alpha m) (c m) = T.adjoint b := by
213   have h := congrArg T (a_normal hm)
214   simpa only [RegularizedHilbertRepair.normal_apply, T_adjoint, map_add, map_smul,
215     c, b] using h
216 
217 /-- The attainable candidate is also the exact universal regularized correction. -/
218 theorem c_eq_correction {m : ℕ} (hm : 1 ≤ m) :
219     c m = RegularizedHilbertRepair.correction T (alpha m) (alpha_pos hm) b :=
220   RegularizedHilbertRepair.normal_unique T (alpha m) (alpha_pos hm) b (c m) (c_normal hm)
221 
222 /-- The attainable bias is exactly the escaping problem's residual vector. -/
223 theorem w_sub_c_eq_v (m : ℕ) : w - c m = v m := residual_eq_v m
224 
225 theorem norm_bias_sq (m : ℕ) : ‖c m - w‖^2 = B m := by
226   rw [norm_sub_rev, w_sub_c_eq_v, norm_v_sq]
227 
228 theorem norm_a_eq_sqrt_A (m : ℕ) : ‖a m‖ = Real.sqrt (A m) := by
229   rw [← norm_a_sq, Real.sqrt_sq (norm_nonneg _)]
230 
231 theorem norm_v_eq_sqrt_B (m : ℕ) : ‖v m‖ = Real.sqrt (B m) := by
232   rw [← norm_v_sq, Real.sqrt_sq (norm_nonneg _)]
233 
234 /-- The profile is evaluated at the correction's actual infinite Hilbert norm. -/
235 theorem budget_at_a_norm {m : ℕ} (hm : 1 ≤ m) :
236     BudgetProfile.beta T w ‖a m‖ = ‖w - T (a m)‖ := by
237   apply le_antisymm (BudgetProfile.beta_le_residual T w (le_refl _))
238   obtain ⟨x, hx, he⟩ := BudgetProfile.exists_budget_minimizer T w (norm_nonneg (a m))
239   rw [← he]
240   rw [a_eq_correction hm] at hx ⊢
241   simpa only [norm_sub_rev] using
242     RegularizedHilbertRepair.residual_best_at_budget T (alpha m) (alpha_pos hm) w x hx
243 
244 /-- Exact identification of the infinite budget profile on the regularized budgets. -/
245 theorem budget_at_sqrt_A {m : ℕ} (hm : 1 ≤ m) :
246     BudgetProfile.beta T w (Real.sqrt (A m)) = Real.sqrt (B m) := by
247   rw [← norm_a_eq_sqrt_A, budget_at_a_norm hm, residual_eq_v, norm_v_eq_sqrt_B]
248 
249 /-- Every actual vector has summable squared real coordinates. -/
250 theorem summable_coordinates_sq (x : H) : Summable (fun j => (x j)^2) := by
251   simpa only [Real.inner_apply, pow_two] using (lp.summable_inner (𝕜 := ℝ) x x)
252 
253 theorem summable_bCoord_sq : Summable (fun j => (bCoord j)^2) := by
254   simpa only [b_apply] using summable_coordinates_sq b
255 
256 theorem summable_cCoord_sq (m : ℕ) : Summable (fun j => (cCoord m j)^2) := by
257   simpa only [c_apply] using summable_coordinates_sq (c m)
258 
259 /-- The hard-prefix correction is a finite sum inside the same infinite Hilbert space. -/
260 def hardPrefix (N : ℕ) : H := ∑ j ∈ Finset.range N, lp.single 2 j (1 : ℝ)
261 
262 @[simp] theorem hardPrefix_apply (N j : ℕ) :
263     hardPrefix N j = if j < N then 1 else 0 := by
264   simp only [hardPrefix, lp.coeFn_sum, Finset.sum_apply, lp.single_apply,
265     Finset.sum_pi_single, Finset.mem_range]
266 
267 /-- Its budget is its actual Hilbert norm, whose square is exactly `N`. -/
268 theorem norm_hardPrefix_sq (N : ℕ) : ‖hardPrefix N‖^2 = (N : ℝ) := by
269   have h := lp.norm_sum_single (p := 2) (by norm_num)
270     (fun _ : ℕ => (1 : ℝ)) (Finset.range N)
271   simpa [hardPrefix, Real.rpow_two] using h
272 
273 theorem norm_hardPrefix (N : ℕ) : ‖hardPrefix N‖ = Real.sqrt (N : ℝ) := by
274   rw [← norm_hardPrefix_sq, Real.sqrt_sq (norm_nonneg _)]
275 
276 @[simp] theorem hardPrefix_residual_apply (N j : ℕ) :
277     (w - T (hardPrefix N)) j = if j < N then 0 else wCoord j := by
278   change wCoord j - wCoord j * hardPrefix N j = _
279   rw [hardPrefix_apply]
280   split_ifs <;> simp
281 
282 /-- The hard-prefix residual square is the genuine omitted infinite reciprocal-square tail. -/
283 theorem norm_hardPrefix_residual_sq (N : ℕ) :
284     ‖w - T (hardPrefix N)‖^2 = ∑' j, (wCoord (j + N))^2 := by
285   let r : H := w - T (hardPrefix N)
286   have hsplit := Summable.sum_add_tsum_nat_add N (summable_coordinates_sq r)
287   have hpre : ∑ j ∈ Finset.range N, (r j)^2 = 0 := by
288     apply Finset.sum_eq_zero
289     intro j hj
290     simp [r, hardPrefix_residual_apply, Finset.mem_range.mp hj]
291   have htail : (∑' j, (r (j + N))^2) = ∑' j, (wCoord (j + N))^2 := by
292     apply tsum_congr
293     intro j
294     have hj : ¬ j + N < N := by omega
295     simp [r, hardPrefix_residual_apply, hj]
296   rw [hpre, zero_add] at hsplit
297   calc
298     ‖r‖^2 = ∑' j, (r j)^2 := norm_sq_eq_tsum r
299     _ = ∑' j, (r (j + N))^2 := hsplit.symm
300     _ = ∑' j, (wCoord (j + N))^2 := htail
301 
302 end KomorebiSpace.DiagonalRegularization

Back to source controls