DiagonalSeriesBounds.lean

1 import KomorebiSpace.DiagonalDefinitions
2 import Mathlib.Analysis.PSeries
3 import Mathlib.Analysis.SpecificLimits.Basic
4 import Mathlib.Tactic
5 
6 set_option autoImplicit false
7 noncomputable section
8 open Filter
9 open scoped Topology
10 namespace KomorebiSpace.DiagonalRegularization
11 
12  theorem index_pos (j : ℕ) : 0 < index j := by
13   unfold index
14   positivity
15 
16  theorem index_ge_one (j : ℕ) : 1 ≤ index j := by
17   unfold index
18   linarith [show (0 : ℝ) ≤ (j : ℝ) from Nat.cast_nonneg j]
19 
20  theorem denominator_pos (m j : ℕ) : 0 < (m : ℝ)^2 + (index j)^2 := by
21   have := sq_pos_of_pos (index_pos j)
22   positivity
23 
24  theorem aCoord_nonneg (m j : ℕ) : 0 ≤ aCoord m j := by
25   unfold aCoord
26   positivity
27 
28  theorem vCoord_nonneg (m j : ℕ) : 0 ≤ vCoord m j := by
29   exact le_of_lt (div_pos (index_pos j) (denominator_pos m j))
30 
31  theorem wCoord_nonneg (j : ℕ) : 0 ≤ wCoord j := by
32   exact inv_nonneg.mpr (index_pos j).le
33 
34  theorem aCoord_le_one (m j : ℕ) : aCoord m j ≤ 1 := by
35   unfold aCoord
36   apply (div_le_one (denominator_pos m j)).mpr
37   nlinarith [sq_nonneg (index j)]
38 
39  theorem aCoord_sq_le_one (m j : ℕ) : aCoord m j ^ 2 ≤ 1 := by
40   simpa using pow_le_pow_left₀ (aCoord_nonneg m j) (aCoord_le_one m j) 2
41 
42  theorem aCoord_le_pseries (m j : ℕ) :
43     aCoord m j ≤ (m : ℝ)^2 / (index j)^2 := by
44   exact div_le_div_of_nonneg_left (sq_nonneg _) (sq_pos_of_pos (index_pos j))
45     (le_add_of_nonneg_left (sq_nonneg _))
46 
47  theorem aCoord_sq_le_pseries (m j : ℕ) :
48     aCoord m j ^ 2 ≤ (m : ℝ)^4 * ((index j)^4)⁻¹ := by
49   calc
50     aCoord m j ^ 2 ≤ ((m : ℝ)^2 / (index j)^2)^2 :=
51       pow_le_pow_left₀ (aCoord_nonneg m j) (aCoord_le_pseries m j) 2
52     _ = (m : ℝ)^4 * ((index j)^4)⁻¹ := by ring
53 
54  theorem vCoord_le_wCoord (m j : ℕ) : vCoord m j ≤ wCoord j := by
55   have hj := index_pos j
56   calc
57     vCoord m j ≤ index j / (index j)^2 := by
58       unfold vCoord
59       apply div_le_div_of_nonneg_left hj.le (sq_pos_of_pos hj)
60       nlinarith [sq_nonneg (m : ℝ)]
61     _ = wCoord j := by
62       unfold wCoord
63       field_simp [ne_of_gt hj]
64 
65  theorem vCoord_sq_le_wCoord_sq (m j : ℕ) :
66     vCoord m j ^ 2 ≤ wCoord j ^ 2 :=
67   pow_le_pow_left₀ (vCoord_nonneg m j) (vCoord_le_wCoord m j) 2
68 
69  theorem summable_index_pow_inv {p : ℕ} (hp : 1 < p) :
70     Summable (fun j : ℕ => ((index j)^p)⁻¹) := by
71   have h := (summable_nat_add_iff 1).2 (Real.summable_nat_pow_inv.mpr hp)
72   simpa [index, Nat.cast_add, Nat.cast_one] using h
73 
74  theorem summable_wCoord_sq : Summable (fun j => wCoord j ^ 2) := by
75   simpa [wCoord, inv_pow] using (summable_index_pow_inv (p := 2) (by norm_num))
76 
77  theorem summable_aCoord_sq (m : ℕ) : Summable (fun j => aCoord m j ^ 2) := by
78   exact Summable.of_nonneg_of_le (fun j => sq_nonneg _) (aCoord_sq_le_pseries m)
79     ((summable_index_pow_inv (p := 4) (by norm_num)).mul_left ((m : ℝ)^4))
80 
81  theorem summable_vCoord_sq (m : ℕ) : Summable (fun j => vCoord m j ^ 2) := by
82   exact Summable.of_nonneg_of_le (fun j => sq_nonneg _) (vCoord_sq_le_wCoord_sq m)
83     summable_wCoord_sq
84 
85 theorem aCoord_sq_lower_prefix (m j : ℕ) (_hm : 1 ≤ m) (hj : j < m) :
86     (1 : ℝ) / 4 ≤ aCoord m j ^ 2 := by
87   have hjm : index j ≤ (m : ℝ) := by
88     simpa [index, Nat.cast_add, Nat.cast_one] using
89       (show ((j + 1 : ℕ) : ℝ) ≤ (m : ℝ) by exact_mod_cast (Nat.succ_le_of_lt hj))
90   have hjnonneg := (index_pos j).le
91   have hs : (index j)^2 ≤ (m : ℝ)^2 := pow_le_pow_left₀ hjnonneg hjm 2
92   have hh : (1 : ℝ) / 2 ≤ aCoord m j := by
93     unfold aCoord
94     apply (le_div_iff₀ (denominator_pos m j)).mpr
95     nlinarith
96   have hsquare := pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 1 / 2) hh 2
97   norm_num at hsquare
98   exact hsquare
99 
100 theorem vCoord_sq_upper_parameter (m j : ℕ) (hm : 1 ≤ m) :
101     vCoord m j ^ 2 ≤ 1 / (m : ℝ)^2 := by
102   have hmpos : 0 < (m : ℝ) := by exact_mod_cast (show 0 < m by omega)
103   have hv : vCoord m j ≤ 1 / (m : ℝ) := by
104     unfold vCoord
105     apply (div_le_div_iff₀ (denominator_pos m j) hmpos).mpr
106     have := sq_nonneg (index j - (m : ℝ))
107     have := mul_nonneg (index_pos j).le hmpos.le
108     nlinarith
109   calc
110     vCoord m j ^ 2 ≤ (1 / (m : ℝ))^2 :=
111       pow_le_pow_left₀ (vCoord_nonneg m j) hv 2
112     _ = 1 / (m : ℝ)^2 := by ring
113 
114 theorem vCoord_sq_lower_tail (m j : ℕ) (hj : m ≤ j) :
115     (1 : ℝ) / 4 * wCoord j ^ 2 ≤ vCoord m j ^ 2 := by
116   have hjm : (m : ℝ) ≤ index j := by
117     have : (m : ℝ) ≤ (j : ℝ) := by exact_mod_cast hj
118     unfold index
119     linarith
120   have hs : (m : ℝ)^2 ≤ (index j)^2 :=
121     pow_le_pow_left₀ (Nat.cast_nonneg m) hjm 2
122   have hv : wCoord j / 2 ≤ vCoord m j := by
123     calc
124       wCoord j / 2 = index j / (2 * (index j)^2) := by
125         unfold wCoord
126         field_simp [ne_of_gt (index_pos j)]
127       _ ≤ vCoord m j := by
128         unfold vCoord
129         apply div_le_div_of_nonneg_left (index_pos j).le (denominator_pos m j)
130         linarith
131   have hsquare := pow_le_pow_left₀ (div_nonneg (wCoord_nonneg j) (by norm_num)) hv 2
132   nlinarith [hsquare]
133 
134 theorem partialA_le_A (m K : ℕ) : partialA m K ≤ A m := by
135   exact Summable.sum_le_tsum (Finset.range K) (fun j _ => sq_nonneg _)
136     (summable_aCoord_sq m)
137 
138 theorem partialB_le_B (m K : ℕ) : partialB m K ≤ B m := by
139   exact Summable.sum_le_tsum (Finset.range K) (fun j _ => sq_nonneg _)
140     (summable_vCoord_sq m)
141 
142 theorem A_lower (m : ℕ) (hm : 1 ≤ m) : (m : ℝ) / 4 ≤ A m := by
143   calc
144     (m : ℝ) / 4 = ∑ j ∈ Finset.range m, (1 : ℝ) / 4 := by simp; ring
145     _ ≤ partialA m m := by
146       apply Finset.sum_le_sum
147       intro j hj
148       exact aCoord_sq_lower_prefix m j hm (Finset.mem_range.mp hj)
149     _ ≤ A m := partialA_le_A m m
150 
151 theorem partialA_upper (m K : ℕ) : partialA m K ≤ (K : ℝ) := by
152   calc
153     partialA m K ≤ ∑ j ∈ Finset.range K, (1 : ℝ) := by
154       exact Finset.sum_le_sum (fun j _ => aCoord_sq_le_one m j)
155     _ = (K : ℝ) := by simp
156 
157 theorem partialB_parameter_upper (m : ℕ) (hm : 1 ≤ m) :
158     partialB m m ≤ 1 / (m : ℝ) := by
159   have hmne : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
160   calc
161     partialB m m ≤ ∑ j ∈ Finset.range m, (1 / (m : ℝ)^2) := by
162       exact Finset.sum_le_sum (fun j _ => vCoord_sq_upper_parameter m j hm)
163     _ = 1 / (m : ℝ) := by simp; field_simp
164 
165 theorem A_sub_partial_eq_tsum (m K : ℕ) :
166     A m - partialA m K = ∑' j, aCoord m (j + K)^2 := by
167   have h := Summable.sum_add_tsum_nat_add K (summable_aCoord_sq m)
168   change partialA m K + (∑' j, aCoord m (j + K)^2) = A m at h
169   linarith
170 
171 theorem B_sub_partial_eq_tsum (m K : ℕ) :
172     B m - partialB m K = ∑' j, vCoord m (j + K)^2 := by
173   have h := Summable.sum_add_tsum_nat_add K (summable_vCoord_sq m)
174   change partialB m K + (∑' j, vCoord m (j + K)^2) = B m at h
175   linarith
176 
177 theorem A_tail_nonneg (m K : ℕ) : 0 ≤ A m - partialA m K := by
178   exact sub_nonneg.mpr (partialA_le_A m K)
179 
180 theorem B_tail_nonneg (m K : ℕ) : 0 ≤ B m - partialB m K := by
181   exact sub_nonneg.mpr (partialB_le_B m K)
182 
183 theorem summable_tail_pseries (K p : ℕ) (hp : 1 < p) :
184     Summable (fun j : ℕ => 1 / ((K : ℝ) + j + 1)^p) := by
185   have h := (summable_nat_add_iff K).2 (summable_index_pow_inv hp)
186   simpa [index, Nat.cast_add, one_div, add_comm, add_left_comm, add_assoc] using h
187 
188 
189 lemma series_tail_sum_range_le_telescope (f g : ℕ → ℝ)
190     (hfg : ∀ j, f j ≤ g j - g (j + 1)) (n : ℕ) :
191     ∑ j ∈ Finset.range n, f j ≤ g 0 - g n := by
192   induction n with
193   | zero => simp
194   | succ n ih =>
195     rw [Finset.sum_range_succ]
196     calc
197       (∑ j ∈ Finset.range n, f j) + f n ≤
198           (g 0 - g n) + (g n - g (n + 1)) := add_le_add ih (hfg n)
199       _ = g 0 - g (n + 1) := by ring
200 
201 lemma series_tail_telescope_le_sum_range (f g : ℕ → ℝ)
202     (hfg : ∀ j, g j - g (j + 1) ≤ f j) (n : ℕ) :
203     g 0 - g n ≤ ∑ j ∈ Finset.range n, f j := by
204   induction n with
205   | zero => simp
206   | succ n ih =>
207     rw [Finset.sum_range_succ]
208     calc
209       g 0 - g (n + 1) = (g 0 - g n) + (g n - g (n + 1)) := by ring
210       _ ≤ (∑ j ∈ Finset.range n, f j) + f n := add_le_add ih (hfg n)
211 
212 lemma series_tail_sq_upper_step (x : ℝ) (hx : 0 < x) :
213     1 / (x + 1)^2 ≤ 1 / x - 1 / (x + 1) := by
214   have hxp : 0 < x + 1 := by linarith
215   have heq : 1 / x - 1 / (x + 1) - 1 / (x + 1)^2 =
216       1 / (x * (x + 1)^2) := by
217     field_simp [ne_of_gt hx, ne_of_gt hxp]; ring
218   have hnonneg : 0 ≤ 1 / (x * (x + 1)^2) := by positivity
219   linarith
220 
221 lemma series_tail_sq_lower_step (x : ℝ) (hx : 0 < x) :
222     1 / x - 1 / (x + 1) ≤ 1 / x^2 := by
223   have hxp : 0 < x + 1 := by linarith
224   have heq : 1 / x^2 - (1 / x - 1 / (x + 1)) =
225       1 / (x^2 * (x + 1)) := by
226     field_simp [ne_of_gt hx, ne_of_gt hxp]; ring
227   have hnonneg : 0 ≤ 1 / (x^2 * (x + 1)) := by positivity
228   linarith
229 
230 lemma series_tail_fourth_upper_step (x : ℝ) (hx : 0 < x) :
231     1 / (x + 1)^4 ≤ 1 / (3 * x^3) - 1 / (3 * (x + 1)^3) := by
232   have hxp : 0 < x + 1 := by linarith
233   have heq : 1 / (3 * x^3) - 1 / (3 * (x + 1)^3) - 1 / (x + 1)^4 =
234       (6*x^2 + 4*x + 1) / (3*x^3*(x + 1)^4) := by
235     field_simp [ne_of_gt hx, ne_of_gt hxp]; ring
236   have hnonneg : 0 ≤ (6*x^2 + 4*x + 1) / (3*x^3*(x + 1)^4) := by positivity
237   linarith
238 
239 lemma series_tail_sq_partial_upper (K n : ℕ) (hK : 1 ≤ K) :
240     ∑ j ∈ Finset.range n, 1 / ((K : ℝ) + j + 1)^2 ≤ 1 / (K : ℝ) := by
241   have hKpos : 0 < (K : ℝ) := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hK)
242   have hstep : ∀ j : ℕ, 1 / ((K : ℝ) + j + 1)^2 ≤
243       1 / ((K : ℝ) + j) - 1 / ((K : ℝ) + (j + 1 : ℕ)) := by
244     intro j
245     simpa only [Nat.cast_add, Nat.cast_one, add_assoc] using
246       series_tail_sq_upper_step ((K : ℝ) + j) (by positivity)
247   have h := series_tail_sum_range_le_telescope
248     (fun j => 1 / ((K : ℝ) + j + 1)^2)
249     (fun j => 1 / ((K : ℝ) + j)) hstep n
250   simp only [Nat.cast_zero, add_zero] at h
251   have hnonneg : 0 ≤ 1 / ((K : ℝ) + n) := by positivity
252   linarith
253 
254 lemma series_tail_fourth_partial_upper (K n : ℕ) (hK : 1 ≤ K) :
255     ∑ j ∈ Finset.range n, 1 / ((K : ℝ) + j + 1)^4 ≤ 1 / (3 * (K : ℝ)^3) := by
256   have hKpos : 0 < (K : ℝ) := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hK)
257   have hstep : ∀ j : ℕ, 1 / ((K : ℝ) + j + 1)^4 ≤
258       1 / (3 * ((K : ℝ) + j)^3) - 1 / (3 * ((K : ℝ) + (j + 1 : ℕ))^3) := by
259     intro j
260     simpa only [Nat.cast_add, Nat.cast_one, add_assoc] using
261       series_tail_fourth_upper_step ((K : ℝ) + j) (by positivity)
262   have h := series_tail_sum_range_le_telescope
263     (fun j => 1 / ((K : ℝ) + j + 1)^4)
264     (fun j => 1 / (3 * ((K : ℝ) + j)^3)) hstep n
265   simp only [Nat.cast_zero, add_zero] at h
266   have hnonneg : 0 ≤ 1 / (3 * ((K : ℝ) + n)^3) := by positivity
267   linarith
268 
269 lemma series_tail_sq_partial_lower (K n : ℕ) :
270     1 / ((K : ℝ) + 1) - 1 / ((K : ℝ) + n + 1) ≤
271       ∑ j ∈ Finset.range n, 1 / ((K : ℝ) + j + 1)^2 := by
272   have hstep : ∀ j : ℕ, 1 / ((K : ℝ) + j + 1) -
273       1 / ((K : ℝ) + (j + 1 : ℕ) + 1) ≤ 1 / ((K : ℝ) + j + 1)^2 := by
274     intro j
275     simpa only [Nat.cast_add, Nat.cast_one, add_assoc] using
276       series_tail_sq_lower_step ((K : ℝ) + j + 1) (by positivity)
277   have h := series_tail_telescope_le_sum_range
278     (fun j => 1 / ((K : ℝ) + j + 1)^2)
279     (fun j => 1 / ((K : ℝ) + j + 1)) hstep n
280   simpa only [Nat.cast_zero, add_zero] using h
281 
282 lemma series_tail_sq_upper (K : ℕ) (hK : 1 ≤ K) :
283     (∑' j : ℕ, 1 / ((K : ℝ) + j + 1)^2) ≤ 1 / (K : ℝ) := by
284   exact Real.tsum_le_of_sum_range_le (fun j => by positivity)
285     (fun n => series_tail_sq_partial_upper K n hK)
286 
287 lemma series_tail_fourth_upper (K : ℕ) (hK : 1 ≤ K) :
288     (∑' j : ℕ, 1 / ((K : ℝ) + j + 1)^4) ≤ 1 / (3 * (K : ℝ)^3) := by
289   exact Real.tsum_le_of_sum_range_le (fun j => by positivity)
290     (fun n => series_tail_fourth_partial_upper K n hK)
291 
292 lemma series_tail_sq_lower (K : ℕ)
293     (hsum : Summable (fun j : ℕ => 1 / ((K : ℝ) + j + 1)^2)) :
294     1 / ((K : ℝ) + 1) ≤ ∑' j : ℕ, 1 / ((K : ℝ) + j + 1)^2 := by
295   have hinv : Tendsto (fun n : ℕ => 1 / ((K : ℝ) + n + 1)) atTop (𝓝 0) := by
296     simpa only [Nat.cast_add, add_comm, add_left_comm, add_assoc] using
297       (tendsto_add_atTop_iff_nat K).2 (tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ))
298   have hleft : Tendsto (fun n : ℕ => 1 / ((K : ℝ) + 1) -
299       1 / ((K : ℝ) + n + 1)) atTop (𝓝 (1 / ((K : ℝ) + 1))) := by
300     simpa only [sub_zero] using (tendsto_const_nhds (x := 1 / ((K : ℝ) + 1))).sub hinv
301   exact le_of_tendsto_of_tendsto' hleft hsum.hasSum.tendsto_sum_nat
302     (fun n => series_tail_sq_partial_lower K n)
303 
304 
305 theorem A_tail_upper (m K : ℕ) (hK : 1 ≤ K) :
306     A m - partialA m K ≤ (m : ℝ)^4 / (3 * (K : ℝ)^3) := by
307   rw [A_sub_partial_eq_tsum]
308   have hcompare : ∀ j : ℕ, aCoord m (j + K)^2 ≤
309       (m : ℝ)^4 * (1 / ((K : ℝ) + j + 1)^4) := by
310     intro j
311     simpa [index, Nat.cast_add, one_div, add_comm, add_left_comm, add_assoc] using
312       aCoord_sq_le_pseries m (j + K)
313   calc
314     (∑' j, aCoord m (j + K)^2) ≤
315         ∑' j : ℕ, (m : ℝ)^4 * (1 / ((K : ℝ) + j + 1)^4) := by
316       exact Summable.tsum_le_tsum hcompare
317         ((summable_nat_add_iff K).2 (summable_aCoord_sq m))
318         ((summable_tail_pseries K 4 (by norm_num)).mul_left _)
319     _ = (m : ℝ)^4 * (∑' j : ℕ, 1 / ((K : ℝ) + j + 1)^4) := by
320       rw [tsum_mul_left]
321     _ ≤ (m : ℝ)^4 * (1 / (3 * (K : ℝ)^3)) := by
322       exact mul_le_mul_of_nonneg_left (series_tail_fourth_upper K hK) (by positivity)
323     _ = (m : ℝ)^4 / (3 * (K : ℝ)^3) := by ring
324 
325 theorem B_tail_upper (m K : ℕ) (hK : 1 ≤ K) :
326     B m - partialB m K ≤ 1 / (K : ℝ) := by
327   rw [B_sub_partial_eq_tsum]
328   have hcompare : ∀ j : ℕ, vCoord m (j + K)^2 ≤
329       1 / ((K : ℝ) + j + 1)^2 := by
330     intro j
331     simpa [index, wCoord, Nat.cast_add, one_div, inv_pow, add_comm, add_left_comm,
332       add_assoc] using vCoord_sq_le_wCoord_sq m (j + K)
333   calc
334     (∑' j, vCoord m (j + K)^2) ≤ ∑' j : ℕ, 1 / ((K : ℝ) + j + 1)^2 := by
335       exact Summable.tsum_le_tsum hcompare
336         ((summable_nat_add_iff K).2 (summable_vCoord_sq m))
337         (summable_tail_pseries K 2 (by norm_num))
338     _ ≤ 1 / (K : ℝ) := series_tail_sq_upper K hK
339 
340 theorem A_upper (m : ℕ) (hm : 1 ≤ m) : A m ≤ 4 * (m : ℝ) / 3 := by
341   have hmne : (m : ℝ) ≠ 0 := by exact_mod_cast (show m ≠ 0 by omega)
342   have ht := A_tail_upper m m hm
343   have hp := partialA_upper m m
344   have heq : (m : ℝ)^4 / (3 * (m : ℝ)^3) = (m : ℝ) / 3 := by
345     field_simp
346   rw [heq] at ht
347   linarith
348 
349 theorem B_upper (m : ℕ) (hm : 1 ≤ m) : B m ≤ 2 / (m : ℝ) := by
350   have ht := B_tail_upper m m hm
351   have hp := partialB_parameter_upper m hm
352   simp only [div_eq_mul_inv] at *
353   linarith
354 
355 theorem B_lower (m : ℕ) : 1 / (4 * ((m : ℝ) + 1)) ≤ B m := by
356   have htail : 1 / ((m : ℝ) + 1) ≤
357       ∑' j : ℕ, 1 / ((m : ℝ) + j + 1)^2 :=
358     series_tail_sq_lower m (summable_tail_pseries m 2 (by norm_num))
359   have hcompare : ∀ j : ℕ, (1 : ℝ) / 4 * (1 / ((m : ℝ) + j + 1)^2) ≤
360       vCoord m (j + m)^2 := by
361     intro j
362     simpa [index, wCoord, Nat.cast_add, one_div, inv_pow, add_comm, add_left_comm,
363       add_assoc] using vCoord_sq_lower_tail m (j + m) (by omega)
364   have hc := Summable.tsum_le_tsum hcompare
365     ((summable_tail_pseries m 2 (by norm_num)).mul_left ((1 : ℝ) / 4))
366     ((summable_nat_add_iff m).2 (summable_vCoord_sq m))
367   rw [tsum_mul_left] at hc
368   have hn : 0 ≤ partialB m m := by
369     exact Finset.sum_nonneg (fun j _ => sq_nonneg _)
370   rw [← B_sub_partial_eq_tsum] at hc
371   have hr : 1 / (4 * ((m : ℝ) + 1)) = (1 : ℝ) / 4 * (1 / ((m : ℝ) + 1)) := by rw [one_div_mul_one_div]
372   rw [hr]
373   linarith
374 
375 theorem proposition_30_1_series (m K : ℕ) (hm : 1 ≤ m) (hmK : m ≤ K) :
376     (m : ℝ) / 4 ≤ A m ∧ A m ≤ 4 * (m : ℝ) / 3 ∧
377     1 / (4 * ((m : ℝ) + 1)) ≤ B m ∧ B m ≤ 2 / (m : ℝ) ∧
378     0 ≤ A m - partialA m K ∧
379     A m - partialA m K ≤ (m : ℝ)^4 / (3 * (K : ℝ)^3) ∧
380     0 ≤ B m - partialB m K ∧ B m - partialB m K ≤ 1 / (K : ℝ) := by
381   have hK : 1 ≤ K := le_trans hm hmK
382   exact ⟨A_lower m hm, A_upper m hm, B_lower m, B_upper m hm,
383     A_tail_nonneg m K, A_tail_upper m K hK, B_tail_nonneg m K, B_tail_upper m K hK⟩
384 
385 end KomorebiSpace.DiagonalRegularization

Back to source controls