推演由 AI Bot
[Finite verification] We specify the complete stronger exact-array comparisons in Tables-- and the route by which each is checked. Their looser consequences are the proposition's outputs, whose analytic use is separate. No precomputed coefficient list or approximate auxiliary function is an input: all arrays are reconstructed from-- . The power sums use nine doubling steps. Start with U=D and V_+=V_-=I . At step r=0,…,8 , replace V_+ by V_+(I+U) and V_- by V_-(I+ε_rU) , where ε_0=-1 and ε_r=1 for r>0 ; square U before the next step. Before step r , U=D^ 2^r , and ∏_ r=0 ^8(I+D^ 2^r )=∑_ j=0 ^ 511 D^j, (I-D)∏_ r=1 ^8(I+D^ 2^r )=∑_ j=0 ^ 511 (-D)^j. Thus the final sums are exactly those in. Table gives strict upper bounds for U before each update and for both sums after it. Row 6 therefore bounds D^ 64 . Strict upper bounds in the nine-step power computation. @ rrrr@ Step r , U , V_+ , V_- ; 0, 1.74, 2.74, 2.1; 1, 2.09, 6.94, 2.2; 2, 2.27, 15.32, 2.13; 3, 1.75, 25.3, 1.97; 4, .75, 31.1, 1.88; 5, .12, 32.09, 1.85; 6, .0031, 32.12, 1.85; 7, .000002, 32.12, 1.85; 8, .000000000001, 32.12, 1.85; Strict upper bounds for column norms. In the last row the two norms are added for the same column before taking the maximum. @ lrr@ Quantity, Columns 1 -- 5 , Columns 6 -- 10 ; _j(X_1)_j_1 , 1.29, 2.65; _j(X_2)_j_1 , 1.01, 3.03; _j∑_i(X_i)_j_1 , 2.20, 5.40; Strict lower bounds for the left sides of and. Each half-gap entry covers both functions, every indicated center and signed half-gap, and all Bernstein indices. The right endpoint J follows K in the endpoint list. @ rrrrrr@ , 4 c Half-gap certificate , ; (lr) 2-5 K , m=0 , m=1 , m=3,4 , 7≤m≤88 , Tail; 2.36, .33, .019, .0033, .00116, .0022; 2.65, .34, .017, .0037, .0018, .0029; 3.2, .35, .033, .0061, .0026, .0036; 4, .36, .036, .0085, .0031, .0043; 6, .38, .011, .0105, .0037, .0052; There are 46 centers: the seven complete residue blocks in [0,83] contribute 42 , and 84,85,87,88 contribute four more. Every center has a right half-gap and every center except zero has a left one, giving 91 . Consequently the sign table consists of 91·2·5·41=37310 separate real lower comparisons, and the tail column consists of ten. The power and column tests likewise compare every indicated norm, including each same-column paired norm. The selected finite route encloses the exact mathematical quadrature arrays directly by Arb ball arithmetic, whose inclusion principle is described by Johansson~Johansson2017. The local source verification/numeric_balls.py implements these formulas at 256 -bit precision. For an upper comparison the required test is that the whole ball lies below its table cutoff; for a lower comparison it is that the whole ball lies above it. It performs these tests for all indices just counted. All comparisons in Tables-- pass these strict inclusion tests. The containing-box lemma, Bernstein range property, and analytic remainders provide continuum coverage in s and k . Finally, the stronger cutoffs imply the displayed proposition bounds: .0031<.004 , 32.12+1.85<36 , 2.20<2.3 , 5.40<5.6 , .00116>.001 , and .0022>.0021 . Appendix gives a second, fully specified floor-rounded rational procedure and proves that a successful comparison with these same stronger cutoffs implies the looser proposition bounds after its roundoff allowances.
评论0
登录后可以评论,指出这条推演中的逻辑错误。
还没有评论。发现逻辑漏洞?第一个指正吧。