DiagonalAsymptotic.lean

1 import KomorebiSpace.InfiniteDiagonalModel
2 import KomorebiSpace.MonotoneBudgetAsymptotic
3 import KomorebiSpace.BudgetProfileGeometry
4 import KomorebiSpace.DiagonalSeriesBounds
5 import Mathlib.Analysis.SumIntegralComparisons
6 import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
7 import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
8 
9 set_option autoImplicit false
10 noncomputable section
11 open Filter Set MeasureTheory
12 open scoped Topology
13 namespace KomorebiSpace.DiagonalRegularization
14 
15 /-- The integrable decreasing kernel whose square controls correction energy. -/
16 def kernelH (x : ℝ) : ℝ := (1 + x ^ 2)⁻¹
17 /-- The correction-energy kernel. -/
18 def kernelF (x : ℝ) : ℝ := (kernelH x) ^ 2
19 
20 lemma kernelH_nonneg (x : ℝ) : 0 ≤ kernelH x := by
21   unfold kernelH
22   positivity
23 
24 lemma kernelH_le_one (x : ℝ) : kernelH x ≤ 1 := by
25   exact inv_le_one_of_one_le₀ (by nlinarith [sq_nonneg x])
26 
27 lemma kernelH_continuous : Continuous kernelH := by
28   unfold kernelH
29   exact (show Continuous (fun x : ℝ => 1 + x ^ 2) from
30     continuous_const.add (continuous_id.pow 2)).inv₀
31     (fun x => ne_of_gt (by nlinarith [sq_nonneg x]))
32 
33 lemma kernelF_continuous : Continuous kernelF := kernelH_continuous.pow 2
34 
35 lemma kernelH_integrable : Integrable kernelH := integrable_inv_one_add_sq
36 
37 lemma kernelF_integrable : Integrable kernelF := by
38   apply kernelH_integrable.mono' kernelF_continuous.aestronglyMeasurable
39   filter_upwards with x
40   rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
41   unfold kernelF
42   nlinarith [kernelH_nonneg x, kernelH_le_one x]
43 
44 lemma kernelH_antitone : AntitoneOn kernelH (Ici 0) := by
45   intro x hx y hy hxy
46   unfold kernelH
47   apply inv_anti₀ (by positivity)
48   nlinarith [sq_le_sq₀ hx hy |>.mpr hxy]
49 
50 lemma kernelF_antitone : AntitoneOn kernelF (Ici 0) := by
51   intro x hx y hy hxy
52   exact (sq_le_sq₀ (kernelH_nonneg y) (kernelH_nonneg x)).mpr
53     (kernelH_antitone hx hy hxy)
54 
55 lemma kernelH_integral : (∫ x in Ioi (0 : ℝ), kernelH x) = Real.pi / 2 := by
56   simp [kernelH]
57 
58 lemma rational_kernel_tendsto :
59     Tendsto (fun x : ℝ => x / (1 + x ^ 2)) atTop (𝓝 0) := by
60   have hi : Tendsto (fun x : ℝ => x⁻¹) atTop (𝓝 (0 : ℝ)) := tendsto_inv_atTop_zero
61   have h : Tendsto (fun x : ℝ => x⁻¹ / (x⁻¹ ^ 2 + 1)) atTop (𝓝 (0 : ℝ)) := by
62     convert! hi.div ((hi.pow 2).add_const 1) (by norm_num : (0 : ℝ)^2 + 1 ≠ 0) using 1
63     norm_num
64   apply h.congr'
65   filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx
66   field_simp
67 
68 lemma kernelF_antiderivative (x : ℝ) :
69     HasDerivAt (fun x : ℝ => (x / (1 + x ^ 2) + Real.arctan x) / 2) (kernelF x) x := by
70   have hden : 1 + x ^ 2 ≠ 0 := by positivity
71   have hd : HasDerivAt (fun x : ℝ => 1 + x ^ 2) (2 * x) x := by
72     convert! ((hasDerivAt_id x).pow 2).const_add 1 using 1
73     norm_num
74   have hh := (((hasDerivAt_id x).div hd hden).add (Real.hasDerivAt_arctan' x)).div_const 2
75   convert! hh using 1
76   unfold kernelF kernelH
77   dsimp
78   field_simp
79   ring
80 
81 lemma kernelF_integral : (∫ x in Ioi (0 : ℝ), kernelF x) = Real.pi / 4 := by
82   have ht : Tendsto (fun x : ℝ => (x / (1 + x ^ 2) + Real.arctan x) / 2)
83       atTop (𝓝 (Real.pi / 4)) := by
84     convert! (rational_kernel_tendsto.add
85       (tendsto_nhds_of_tendsto_nhdsWithin Real.tendsto_arctan_atTop)).div_const 2 using 1
86     ring_nf
87   have hi := integral_Ioi_of_hasDerivAt_of_tendsto'
88     (fun x (_ : x ∈ Ici (0 : ℝ)) => kernelF_antiderivative x)
89     kernelF_integrable.integrableOn ht
90   simpa using hi
91 
92 /-- Scaled positive-integer samples, without replacing the infinite series by a truncation. -/
93 def rightSum (k : ℝ → ℝ) (m : ℝ) : ℝ := (∑' n : ℕ, k (((n : ℝ) + 1) / m)) / m
94 
95 lemma scaled_kernel_integrable {k : ℝ → ℝ} (hk : Integrable k) {m : ℝ} (hm : 0 < m) :
96     Integrable (fun x : ℝ => k (x / m)) := by
97   convert! hk.comp_mul_left' (inv_ne_zero hm.ne') using 1
98   ext x
99   congr 1
100   ring
101 
102 lemma scaled_kernel_integral (k : ℝ → ℝ) {m : ℝ} (hm : 0 < m) :
103     (∫ x in Ioi (0 : ℝ), k (x / m)) = m * ∫ x in Ioi (0 : ℝ), k x := by
104   simpa only [div_eq_mul_inv, inv_inv, zero_mul, smul_eq_mul] using
105     integral_comp_mul_right_Ioi k 0 (inv_pos.mpr hm)
106 
107 /-- The right-sampling error of a nonnegative decreasing kernel is at most its
108 initial height divided by the scale. -/
109 lemma rightSum_bounds {k : ℝ → ℝ} (hk : Integrable k)
110     (ha : AntitoneOn k (Ici 0)) (hn : ∀ x, 0 ≤ k x) {m : ℝ} (hm : 0 < m) :
111     (∫ x in Ioi (0 : ℝ), k x) - k 0 / m ≤ rightSum k m ∧
112     rightSum k m ≤ ∫ x in Ioi (0 : ℝ), k x := by
113   have hi := (scaled_kernel_integrable hk hm).integrableOn (s := Ioi 0)
114   have ha' : AntitoneOn (fun x : ℝ => k (x / m)) (Ici 0) := by
115     intro x hx y hy hxy
116     exact ha (div_nonneg hx hm.le) (div_nonneg hy hm.le)
117       (div_le_div_of_nonneg_right hxy hm.le)
118   have hn' : ∀ x ∈ Ioi (0 : ℝ), 0 ≤ k (x / m) := fun x _ => hn _
119   have hs := ha'.summable_of_integrableOn_Ioi_zero hi hn'
120   have hu := ha'.tsum_add_one_le_integral hi hn'
121   have hl := ha'.integral_le_tsum hs hn'
122   rw [scaled_kernel_integral k hm] at hu hl
123   rw [hs.tsum_eq_zero_add] at hl
124   simp only [Nat.cast_zero, zero_div, Nat.cast_add, Nat.cast_one] at hu hl
125   unfold rightSum
126   constructor
127   · apply (le_div_iff₀ hm).mpr
128     calc
129       ((∫ x in Ioi (0 : ℝ), k x) - k 0 / m) * m =
130           m * (∫ x in Ioi (0 : ℝ), k x) - k 0 := by field_simp
131       _ ≤ ∑' n : ℕ, k (((n : ℝ) + 1) / m) := by linarith
132   · apply (div_le_iff₀ hm).mpr
133     simpa only [mul_comm] using hu
134 
135 lemma rightSum_tendsto {k : ℝ → ℝ} (hk : Integrable k)
136     (ha : AntitoneOn k (Ici 0)) (hn : ∀ x, 0 ≤ k x) :
137     Tendsto (fun m : ℕ => rightSum k m) atTop (𝓝 (∫ x in Ioi (0 : ℝ), k x)) := by
138   have hlo : Tendsto (fun m : ℕ => (∫ x in Ioi (0 : ℝ), k x) - k 0 / m)
139       atTop (𝓝 (∫ x in Ioi (0 : ℝ), k x)) := by
140     simpa using tendsto_const_nhds.sub (tendsto_const_div_atTop_nhds_zero_nat (k 0))
141   apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hlo tendsto_const_nhds
142   · filter_upwards [eventually_ge_atTop 1] with m hm
143     exact (rightSum_bounds hk ha hn (by exact_mod_cast (show 0 < m by omega))).1
144   · filter_upwards [eventually_ge_atTop 1] with m hm
145     exact (rightSum_bounds hk ha hn (by exact_mod_cast (show 0 < m by omega))).2
146 
147 lemma kernelF_sample {m : ℕ} (hm : 1 ≤ m) (j : ℕ) :
148     kernelF (((j : ℝ) + 1) / m) = (aCoord m j)^2 := by
149   have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
150   have hd := ne_of_gt (denominator_pos m j)
151   unfold kernelF kernelH aCoord index at *
152   field_simp
153 
154 lemma kernelH_sample {m : ℕ} (hm : 1 ≤ m) (j : ℕ) :
155     kernelH (((j : ℝ) + 1) / m) = (aCoord m j)^2 + (m : ℝ)^2 * (vCoord m j)^2 := by
156   have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
157   have hd := ne_of_gt (denominator_pos m j)
158   unfold kernelH aCoord vCoord index at *
159   field_simp
160 
161 lemma A_div_eq_rightSum {m : ℕ} (hm : 1 ≤ m) : A m / m = rightSum kernelF m := by
162   unfold A rightSum
163   congr 1
164   exact tsum_congr (fun j => (kernelF_sample hm j).symm)
165 
166 lemma mul_B_eq_rightSum_sub {m : ℕ} (hm : 1 ≤ m) :
167     (m : ℝ) * B m = rightSum kernelH m - rightSum kernelF m := by
168   have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
169   rw [← A_div_eq_rightSum hm]
170   unfold rightSum
171   rw [tsum_congr (kernelH_sample hm)]
172   rw [(summable_aCoord_sq m).tsum_add ((summable_vCoord_sq m).mul_left ((m : ℝ)^2))]
173   rw [(summable_vCoord_sq m).tsum_mul_left]
174   change (m : ℝ) * B m = (A m + (m : ℝ)^2 * B m) / m - A m / m
175   field_simp
176   ring
177 
178 /-- The actual infinite correction energy has leading coefficient pi/4. -/
179 theorem tendsto_A_div : Tendsto (fun m : ℕ => A m / m) atTop (𝓝 (Real.pi / 4)) := by
180   have h := rightSum_tendsto kernelF_integrable kernelF_antitone (fun x => sq_nonneg (kernelH x))
181   rw [kernelF_integral] at h
182   apply h.congr'
183   filter_upwards [eventually_ge_atTop 1] with m hm
184   exact (A_div_eq_rightSum hm).symm
185 
186 /-- The actual infinite residual energy has leading coefficient pi/4. -/
187 theorem tendsto_mul_B : Tendsto (fun m : ℕ => (m : ℝ) * B m) atTop (𝓝 (Real.pi / 4)) := by
188   have hh := rightSum_tendsto kernelH_integrable kernelH_antitone kernelH_nonneg
189   have hf := rightSum_tendsto kernelF_integrable kernelF_antitone (fun x => sq_nonneg (kernelH x))
190   rw [kernelH_integral] at hh
191   rw [kernelF_integral] at hf
192   have h : Tendsto (fun m : ℕ => rightSum kernelH m - rightSum kernelF m)
193       atTop (𝓝 (Real.pi / 4)) := by
194     convert! hh.sub hf using 1
195     ring_nf
196   apply h.congr'
197   filter_upwards [eventually_ge_atTop 1] with m hm
198   exact (mul_B_eq_rightSum_sub hm).symm
199 
200 lemma A_nonneg (m : ℕ) : 0 ≤ A m := tsum_nonneg (fun _ => sq_nonneg _)
201 lemma B_nonneg (m : ℕ) : 0 ≤ B m := tsum_nonneg (fun _ => sq_nonneg _)
202 
203 lemma A_pos {m : ℕ} (hm : 1 ≤ m) : 0 < A m := by
204   have hmp : (0 : ℝ) < m := by exact_mod_cast (show 0 < m by omega)
205   exact lt_of_lt_of_le (div_pos hmp (by norm_num)) (A_lower m hm)
206 
207 lemma aCoord_monotone (j : ℕ) : Monotone (fun m => aCoord m j) := by
208   intro m n hmn
209   have hsq : (m : ℝ)^2 ≤ (n : ℝ)^2 :=
210     (sq_le_sq₀ (Nat.cast_nonneg m) (Nat.cast_nonneg n)).mpr (by exact_mod_cast hmn)
211   unfold aCoord
212   apply (div_le_div_iff₀ (denominator_pos m j) (denominator_pos n j)).mpr
213   nlinarith [mul_nonneg (sub_nonneg.mpr hsq) (sq_nonneg (index j))]
214 
215 lemma A_monotone : Monotone A := by
216   intro m n hmn
217   exact Summable.tsum_le_tsum (fun j => (sq_le_sq₀ (aCoord_nonneg m j) (aCoord_nonneg n j)).mpr
218     (aCoord_monotone j hmn)) (summable_aCoord_sq m) (summable_aCoord_sq n)
219 
220 lemma A_tendsto_atTop : Tendsto A atTop atTop := by
221   apply tendsto_atTop_mono' atTop ?_
222     ((tendsto_natCast_atTop_atTop : Tendsto (fun m : ℕ => (m : ℝ)) atTop atTop).atTop_div_const (by norm_num : (0 : ℝ) < 4))
223   filter_upwards [eventually_ge_atTop 1] with m hm
224   exact A_lower m hm
225 
226 lemma A_successor_ratio_tendsto :
227     Tendsto (fun m : ℕ => A (m+1) / A m) atTop (𝓝 1) := by
228   have hc : Real.pi / 4 ≠ 0 := ne_of_gt (div_pos Real.pi_pos (by norm_num))
229   have hn : Tendsto (fun m : ℕ => A (m+1) / ((m+1 : ℕ) : ℝ)) atTop (𝓝 (Real.pi / 4)) :=
230     tendsto_A_div.comp (tendsto_add_atTop_nat 1)
231   have hrat : Tendsto (fun m : ℕ => ((m : ℝ)+1) / m) atTop (𝓝 1) := by
232     convert! tendsto_add_mul_div_add_mul_atTop_nhds (1 : ℝ) 0 1 (by norm_num : (1 : ℝ) ≠ 0) using 1 <;> simp [add_comm]
233   have h : Tendsto (fun m : ℕ =>
234       (A (m+1) / ((m+1 : ℕ) : ℝ)) / (A m / m) * (((m : ℝ)+1) / m)) atTop (𝓝 1) := by
235     convert! (hn.div tendsto_A_div hc).mul hrat using 1
236     simp [hc]
237   apply h.congr'
238   filter_upwards [eventually_ge_atTop 1] with m hm
239   have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
240   have hn0 : (m : ℝ) + 1 ≠ 0 := by positivity
241   have ha0 : A m ≠ 0 := ne_of_gt (A_pos hm)
242   push_cast
243   field_simp
244 
245 lemma sqrt_A_mul_sqrt_B_tendsto :
246     Tendsto (fun m : ℕ => Real.sqrt (A m) * Real.sqrt (B m)) atTop (𝓝 (Real.pi / 4)) := by
247   have h : Tendsto (fun m : ℕ => Real.sqrt ((A m / m) * ((m : ℝ) * B m)))
248       atTop (𝓝 (Real.pi / 4)) := by
249     have ht := Real.continuous_sqrt.continuousAt.tendsto.comp (tendsto_A_div.mul tendsto_mul_B)
250     simpa only [Function.comp_def, Real.sqrt_mul_self (by positivity : 0 ≤ Real.pi / 4)] using ht
251   apply h.congr'
252   filter_upwards [eventually_ge_atTop 1] with m hm
253   have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
254   rw [← Real.sqrt_mul (A_nonneg m)]
255   congr 1
256   field_simp
257 
258 /-- A strictly positive mesh of actual correction norms. -/
259 def budgetMesh (n : ℕ) : ℝ := Real.sqrt (A (n+1))
260 
261 lemma budgetMesh_pos (n : ℕ) : 0 < budgetMesh n := Real.sqrt_pos.mpr (A_pos (by omega))
262 
263 lemma budgetMesh_monotone : Monotone budgetMesh := by
264   intro m n hmn
265   exact Real.sqrt_le_sqrt (A_monotone (Nat.add_le_add_right hmn 1))
266 
267 lemma budgetMesh_tendsto_atTop : Tendsto budgetMesh atTop atTop :=
268   Real.tendsto_sqrt_atTop.comp (A_tendsto_atTop.comp (tendsto_add_atTop_nat 1))
269 
270 lemma budgetMesh_ratio_tendsto :
271     Tendsto (fun n => budgetMesh (n+1) / budgetMesh n) atTop (𝓝 1) := by
272   have h := Real.continuous_sqrt.continuousAt.tendsto.comp
273     (A_successor_ratio_tendsto.comp (tendsto_add_atTop_nat 1))
274   simpa only [Function.comp_def, Real.sqrt_one, Real.sqrt_div (A_nonneg _), budgetMesh] using h
275 
276 lemma budgetMesh_product_tendsto :
277     Tendsto (fun n => budgetMesh n * BudgetProfile.beta T w (budgetMesh n))
278       atTop (𝓝 (Real.pi / 4)) := by
279   have h := sqrt_A_mul_sqrt_B_tendsto.comp (tendsto_add_atTop_nat 1)
280   convert! h using 1
281   ext n
282   rw [budgetMesh, budget_at_sqrt_A (by omega)]
283   rfl
284 
285 /-- The limit holds over all real correction budgets, not only the regularization mesh. -/
286 theorem tendsto_actual_budget_product :
287     Tendsto (fun M : ℝ => M * BudgetProfile.beta T w M) atTop (𝓝 (Real.pi / 4)) := by
288   apply tendsto_budget_product_of_mesh budgetMesh (BudgetProfile.beta T w) (Real.pi / 4)
289     budgetMesh_pos budgetMesh_monotone budgetMesh_tendsto_atTop
290   · intro x hx y hy hxy
291     exact BudgetProfileGeometry.beta_antitone T w hx hxy
292   · intro M hM
293     exact BudgetProfile.beta_nonneg T w M
294   · exact budgetMesh_ratio_tendsto
295   · exact budgetMesh_product_tendsto
296 
297 /-- The omitted reciprocal-square energy after a hard prefix. -/
298 def hardPrefixTail (N : ℕ) : ℝ := ∑' j, (wCoord (j + N))^2
299 
300 lemma hardPrefixTail_eq_pseries (N : ℕ) :
301     hardPrefixTail N = ∑' j : ℕ, 1 / ((N : ℝ) + j + 1)^2 := by
302   apply tsum_congr
303   intro j
304   simp [wCoord, index, Nat.cast_add, one_div, inv_pow, add_comm]
305 
306 lemma hardPrefixTail_bounds (N : ℕ) (hN : 1 ≤ N) :
307     1 / ((N : ℝ)+1) ≤ hardPrefixTail N ∧ hardPrefixTail N ≤ 1 / (N : ℝ) := by
308   rw [hardPrefixTail_eq_pseries]
309   exact ⟨series_tail_sq_lower N (summable_tail_pseries N 2 (by norm_num)),
310     series_tail_sq_upper N hN⟩
311 
312 lemma mul_hardPrefixTail_tendsto :
313     Tendsto (fun N : ℕ => (N : ℝ) * hardPrefixTail N) atTop (𝓝 1) := by
314   apply tendsto_of_tendsto_of_tendsto_of_le_of_le'
315     (tendsto_natCast_div_add_atTop (1 : ℝ)) tendsto_const_nhds
316   · filter_upwards [eventually_ge_atTop 1] with N hN
317     have h := mul_le_mul_of_nonneg_left (hardPrefixTail_bounds N hN).1 (Nat.cast_nonneg N : (0 : ℝ) ≤ N)
318     simpa only [mul_one_div] using h
319   · filter_upwards [eventually_ge_atTop 1] with N hN
320     have hn0 : (N : ℝ) ≠ 0 := by exact_mod_cast (show N ≠ 0 by omega)
321     have h := mul_le_mul_of_nonneg_left (hardPrefixTail_bounds N hN).2 (Nat.cast_nonneg N : (0 : ℝ) ≤ N)
322     simpa [hn0] using h
323 
324 /-- The hard-prefix residual product tends to one at its actual correction norm budget. -/
325 theorem tendsto_hardPrefix_product :
326     Tendsto (fun N : ℕ => ‖hardPrefix N‖ * ‖w - T (hardPrefix N)‖) atTop (𝓝 1) := by
327   have h := Real.continuous_sqrt.continuousAt.tendsto.comp mul_hardPrefixTail_tendsto
328   have hr (N : ℕ) : ‖w - T (hardPrefix N)‖ = Real.sqrt (hardPrefixTail N) := by
329     unfold hardPrefixTail
330     rw [← norm_hardPrefix_residual_sq, Real.sqrt_sq (norm_nonneg _)]
331   simpa only [Function.comp_def, Real.sqrt_one, norm_hardPrefix, hr,
332     Real.sqrt_mul (Nat.cast_nonneg _)] using h
333 
334 theorem tendsto_sqrt_mul_hardPrefix_residual :
335     Tendsto (fun N : ℕ => Real.sqrt (N : ℝ) * ‖w - T (hardPrefix N)‖) atTop (𝓝 1) := by
336   simpa only [norm_hardPrefix] using tendsto_hardPrefix_product
337 
338 /-- All four conclusions of the printed sharp diagonal budget theorem, with the
339 budget profile and prefix residual interpreted in the actual infinite Hilbert model. -/
340 theorem sharp_diagonal_budget_asymptotic :
341     Tendsto (fun m : ℕ => A m / m) atTop (𝓝 (Real.pi / 4)) ∧
342     Tendsto (fun m : ℕ => (m : ℝ) * B m) atTop (𝓝 (Real.pi / 4)) ∧
343     Tendsto (fun M : ℝ => M * BudgetProfile.beta T w M) atTop (𝓝 (Real.pi / 4)) ∧
344     Tendsto (fun N : ℕ => Real.sqrt (N : ℝ) * ‖w - T (hardPrefix N)‖) atTop (𝓝 1) :=
345   ⟨tendsto_A_div, tendsto_mul_B, tendsto_actual_budget_product,
346     tendsto_sqrt_mul_hardPrefix_residual⟩
347 
348 end KomorebiSpace.DiagonalRegularization

Back to source controls