Stat.CLT.BerryEsseen.PrawitzHighRationalCertificate
The kernel square table is shared across parameter cells.
PrawitzHighRationalCertificate 1 core · 1 supporting The kernel square table is shared across parameter cells. ★ prawitz_high_rational_sum_certificate
Finite rational certificates for the rescaled high Prawitz sum
The kernel square table is shared across parameter cells. The raw integral sum retains endpoint cubic damping and the exact bandwidth proportional to the lower parameter. Both obligations involve rational arithmetic only and import neither compact allocation nor any open cutoff certificate.
theorem prawitz_high_rational_sum_certificate reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
On each of the 270 explicit compact parameter cells, the complete outward-rounded raw high-frequency rational sum is at most nine fiftieths, which gives the original three-twentieths allocation.
Formal statement
Proof (Lean source)
theorem prawitz_high_rational_sum_certificate (j : Fin 270) :
prawitzRationalHighSum j.val ≤ (9 / 50 : ℚ) := by
/- Lowest open layer: EXACT finite rational sums only. Rounding UP to
a common denominator makes the total an integer bound. Generate checked
blockwise certificates if computing a full row is expensive; do not use
native_decide, new axioms, or assumptions asserting this total.
Exploratory DOUBLE arithmetic found a maximum about 0.177099 near
rho=0.565 before rounding. Up to 999 outward cell roundings add less
than 0.00000999. This supplies a feasibility check, NOT a proof.
Later assembly: the cutoff certificate gives U*I/1000<=U0. Extend
the nonnegative integral down to U*I/1000 and partition through U.
Apply the two proved PrawitzRescaledCells integrals, switching at
i=500. Use the rational pi bounds and the square certificate to
enclose their sqrt factors by the integer table. The denominator
in the lower kernel formula is positive throughout b<=1/2; compare
its numerator using pi>=314159/100000 and pi<=314160/100000. The
endpoint negative cubic exponent is exactly -e, so the reciprocal
Taylor comparison gives each displayed rational cell. Summing and
multiplying by 5*rho/6 gives <=3*rho/20. This numerical leaf is
independent of the cutoff and integral adapters. -/
have hblocks (b : Fin 27) (l : Fin 10) :
highIntSuffix (10 * b.val + l.val)
(1000 - prawitzHighCutoffIndex (10 * b.val + l.val)) ≤ 18000000 := by
fin_cases b
· exact highInteger_block00 l
· exact highInteger_block01 l
· exact highInteger_block02 l
· exact highInteger_block03 l
· exact highInteger_block04 l
· exact highInteger_block05 l
· exact highInteger_block06 l
· exact highInteger_block07 l
· exact highInteger_block08 l
· exact highInteger_block09 l
· exact highInteger_block10 l
· exact highInteger_block11 l
· exact highInteger_block12 l
· exact highInteger_block13 l
· exact highInteger_block14 l
· exact highInteger_block15 l
· exact highInteger_block16 l
· exact highInteger_block17 l
· exact highInteger_block18 l
· exact highInteger_block19 l
· exact highInteger_block20 l
· exact highInteger_block21 l
· exact highInteger_block22 l
· exact highInteger_block23 l
· exact highInteger_block24 l
· exact highInteger_block25 l
· exact highInteger_block26 l
let b : Fin 27 := ⟨j.val / 10, by omega⟩
let l : Fin 10 := ⟨j.val % 10, Nat.mod_lt _ (by decide)⟩
have hj : 10 * b.val + l.val = j.val := by
dsimp [b, l]
omega
have h := hblocks b l
rw [hj] at h
have hcut : ∀ k : Fin 270, prawitzHighCutoffIndex k.val ≤ 1000 := by
decide +kernel
have hk := hcut j
rw [highIntSuffix_sum _ _ (by omega), Nat.sub_sub_self hk] at h
simp only [highCellInteger_eq] at h
have hc : ((∑ i ∈ Ico (prawitzHighCutoffIndex j.val) 1000,
⌈100000000 * prawitzRationalHighCell j.val i⌉ : ℤ) : ℚ) ≤ 18000000 := by
exact_mod_cast h
push_cast at hc
unfold prawitzRationalHighSum prawitzRoundUp
simp only [div_eq_mul_inv, ← Finset.sum_mul]
linarith
1 supporting declaration (lemmas, instances)
-
prawitz_kernel_rational_square_certificatetheorem — On every positive kernel grid cell, the rational squared kernel enclosure is bounded by the square of its explicit outward integer magnitude enclosure.hypothesesi :ℕhi :i ∈ Ico 1 1000conclusionprawitzRationalKernelSq i ≤ ((prawitzKernelMagnitudeIndex i : ℚ) / 1000000) ^ 2Proof (Lean source)
theorem prawitz_kernel_rational_square_certificate (i : ℕ) (hi : i ∈ Ico 1 1000) : prawitzRationalKernelSq i ≤ ((prawitzKernelMagnitudeIndex i : ℚ) / 1000000) ^ 2 := by /- Finite rational arithmetic, no analytic norm calculation here. Unfold the explicit table and split indices below/above 500, then use checked norm_num/decide proofs. Every one of these 999 inequalities has passed an independent Python Fraction sanity check; that is NOT a Lean proof. Preserve the one-millionth magnitude rounding. At index 500 use the reflected upper polynomial, and leave the assigned outer kernel value unchanged: the later norm comparison excludes it only a.e. -/ obtain ⟨hil, hiu⟩ := Finset.mem_Ico.mp hi have hblocks (b : Fin 20) (l : Fin 50) : prawitzRationalKernelSq (1 + 50 * b.val + l.val) ≤ ((prawitzKernelMagnitudeIndex (1 + 50 * b.val + l.val) : ℚ) / 1000000) ^ 2 := by fin_cases b · exact kernelSquare_block00 l · exact kernelSquare_block01 l · exact kernelSquare_block02 l · exact kernelSquare_block03 l · exact kernelSquare_block04 l · exact kernelSquare_block05 l · exact kernelSquare_block06 l · exact kernelSquare_block07 l · exact kernelSquare_block08 l · exact kernelSquare_block09 l · exact kernelSquare_block10 l · exact kernelSquare_block11 l · exact kernelSquare_block12 l · exact kernelSquare_block13 l · exact kernelSquare_block14 l · exact kernelSquare_block15 l · exact kernelSquare_block16 l · exact kernelSquare_block17 l · exact kernelSquare_block18 l · exact kernelSquare_block19 l let b : Fin 20 := ⟨(i - 1) / 50, by omega⟩ let l : Fin 50 := ⟨(i - 1) % 50, Nat.mod_lt _ (by decide)⟩ have he : 1 + 50 * b.val + l.val = i := by dsimp [b, l] omega simpa only [he] using hblocks b l
Core 9 core · 0 supporting Integer numerators, the cached kernel magnitude table, the rounded high-cell integers and their suffix sums.
High Prawitz certificate: integer cell arithmetic
Integer numerators, the cached kernel magnitude table, the rounded high-cell integers and their suffix sums. These are the definitions that the kernel-checked blocks reduce.
def highTaylorNum reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The integer Taylor numerator at integers n and d is the sum over k from 0 to 15 of (15!/k!)·nᵏ·d^(15−k), written in Horner form. For d ≠ 0 it equals 15!·d¹⁵ times the sixteen-term Taylor polynomial of the exponential at n/d.
Definition (Lean source)
parameters
n d :
ℤ
def
highTaylorNum n d :
ℤ
given by
(1307674368000 * d ^ 15 + n * (1307674368000 * d ^ 14 + n * (653837184000 * d ^ 13 + n * (217945728000 * d ^ 12 + n * (54486432000 * d ^ 11 + n * (10897286400 * d ^ 10 + n * (1816214400 * d ^ 9 + n * (259459200 * d ^ 8 + n * (32432400 * d ^ 7 + n * (3603600 * d ^ 6 + n * (360360 * d ^ 5 + n * (32760 * d ^ 4 + n * (2730 * d ^ 3 + n * (210 * d ^ 2 + n * (15 * d ^ 1 + n * 1)))))))))))))))
def highCubic reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The integer cubic damping value at grid index i is 1800000·i² − 1728·i³. Divided by 625000000000 it equals 72a²/25 − 1728a³/625 at the kernel grid point a = i/1000.
Definition (Lean source)
parameters
i :
ℕ
def
highCubic i :
ℤ
given by
1800000 * (i : ℤ) ^ 2 - 1728 * (i : ℤ) ^ 3
def highExponentNum reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The integer numerator of the high-cell exponent for parameter cell j and frequency index i is the smaller of the cubic damping values at i and i + 1, multiplied by the square of the denominator of the cell's right endpoint.
Definition (Lean source)
parameters
j i :
ℕ
def
highExponentNum j i :
ℤ
given by
def highExponentDen reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The integer denominator of the high-cell exponent for parameter cell j is 625000000000 times the square of the numerator of the cell's right endpoint. The exponent numerator over this denominator is the rational exponent used by the high cell bound.
Definition (Lean source)
def highCeil reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The ceiling of the integer fraction n/d computed by integer division: −⌊−n/d⌋ when d ≥ 0 and −⌊n/(−d)⌋ when d < 0. A zero denominator gives zero.
Definition (Lean source)
parameters
n d :
ℤ
def
highCeil n d :
ℤ
given by
if 0 ≤ d then -(-n / d) else -(n / -d)
def highKernelBlock reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The b-th block of thirty-two consecutive entries of the integer kernel magnitude table, for b from 0 to 31 (the last block holds eight entries); any other block number gives the empty array. The blocks are a copy of the table arranged for fast lookup.
Definition (Lean source)
parameters
b :
ℕ
def
given by
match b with | 0
=> #[ 0, 159156123, 79578712, 53053078, 39790387, 31832872, 26527944, 22738779, 19896965, 17686718, 15918567, 14471940, 13266455, 12246464, 11372218, 10614567, 9951650, 9366748, 8846858, 8381715, 7963107, 7584386, 7240111, 6925791, 6637680, 6372634, 6127989, 5901481, 5691164, 5495365, 5312630, 5141696 ] | 1 => #[ 4981456, 4830938, 4689283, 4555733, 4429610, 4310314, 4197305, 4090098, 3988260, 3891396, 3799152, 3711205, 3627262, 3547056, 3470343, 3396900, 3326522, 3259022, 3194227, 3131978, 3072128, 3014541, 2959090, 2905661, 2854143, 2804437, 2756448, 2710090, 2665280, 2621943, 2580007, 2539405 ] | 2 => #[ 2500075, 2461958, 2424998, 2389144, 2354348, 2320562, 2287743, 2255852, 2224848, 2194696, 2165360, 2136809, 2109011, 2081936, 2055557, 2029848, 2004782, 1980337, 1956490, 1933218, 1910502, 1888321, 1866657, 1845492, 1824810, 1804592, 1784825, 1765494, 1746583, 1728079, 1709970, 1692243 ] | 3 => #[ 1674885, 1657886, 1641235, 1624920, 1608932, 1593260, 1577897, 1562832, 1548057, 1533563, 1519343, 1505389, 1491694, 1478250, 1465050, 1452088, 1439358, 1426853, 1414567, 1402495, 1390630, 1378969, 1367505, 1356233, 1345149, 1334248, 1323525, 1312976, 1302597, 1292384, 1282332, 1272439 ] | 4 => #[ 1262699, 1253110, 1243668, 1234370, 1225212, 1216192, 1207305, 1198550, 1189922, 1181420, 1173041, 1164782, 1156640, 1148612, 1140697, 1132893, 1125195, 1117604, 1110115, 1102728, 1095440, 1088249, 1081152, 1074150, 1067238, 1060416, 1053682, 1047034, 1040470, 1033989, 1027589, 1021268 ] | 5 => #[ 1015026, 1008861, 1002770, 996754, 990809, 984936, 979133, 973398, 967731, 962130, 956593, 951121, 945711, 940362, 935074, 929846, 924675, 919562, 914506, 909505, 904558, 899666, 894825, 890037, 885299, 880612, 875974, 871385, 866843, 862348, 857899, 853496 ] | 6 => #[ 849138, 844823, 840552, 836324, 832137, 827992, 823888, 819823, 815798, 811812, 807865, 803955, 800082, 796246, 792446, 788681, 784951, 781256, 777595, 773967, 770373, 766811, 763281, 759782, 756315, 752878, 749472, 746096, 742749, 739431, 736142, 732881 ] | 7 => #[ 729648, 726442, 723264, 720112, 716987, 713887, 710814, 707766, 704742, 701744, 698770, 695819, 692893, 689990, 687110, 684253, 681419, 678606, 675816, 673048, 670300, 667574, 664869, 662184, 659520, 656876, 654252, 651647, 649062, 646496, 643949, 641420 ] | 8 => #[ 638910, 636418, 633945, 631489, 629050, 626629, 624225, 621839, 619468, 617115, 614778, 612457, 610152, 607863, 605589, 603332, 601089, 598861, 596649, 594451, 592268, 590099, 587944, 585804, 583678, 581565, 579466, 577381, 575309, 573250, 571204, 569172 ] | 9 => #[ 567152, 565144, 563150, 561167, 559197, 557239, 555293, 553359, 551436, 549526, 547626, 545739, 543862, 541996, 540142, 538298, 536466, 534644, 532832, 531031, 529241, 527460, 525690, 523930, 522180, 520440, 518709, 516988, 515277, 513575, 511883, 510200 ] | 10 => #[ 508526, 506861, 505205, 503558, 501920, 500291, 498670, 497058, 495454, 493859, 492272, 490694, 489123, 487561, 486007, 484461, 482922, 481392, 479869, 478354, 476846, 475346, 473853, 472368, 470890, 469419, 467956, 466499, 465050, 463607, 462172, 460743 ] | 11 => #[ 459321, 457906, 456498, 455096, 453701, 452312, 450929, 449553, 448184, 446820, 445463, 444112, 442767, 441428, 440095, 438768, 437446, 436131, 434822, 433518, 432220, 430927, 429640, 428359, 427083, 425812, 424547, 423287, 422033, 420784, 419540, 418301 ] | 12 => #[ 417067, 415838, 414615, 413396, 412182, 410974, 409770, 408571, 407376, 406187, 405002, 403821, 402646, 401475, 400308, 399146, 397989, 396836, 395687, 394543, 393403, 392267, 391136, 390008, 388885, 387767, 386652, 385541, 384434, 383332, 382233, 381138 ] | 13 => #[ 380047, 378960, 377877, 376798, 375723, 374651, 373583, 372518, 371458, 370401, 369347, 368298, 367251, 366209, 365169, 364133, 363101, 362072, 361046, 360024, 359005, 357990, 356977, 355968, 354962, 353959, 352960, 351963, 350970, 349980, 348993, 348009 ] | 14 => #[ 347028, 346049, 345074, 344102, 343133, 342166, 341203, 340242, 339284, 338329, 337377, 336427, 335481, 334537, 333595, 332656, 331720, 330787, 329856, 328928, 328002, 327079, 326158, 325240, 324324, 323411, 322500, 321592, 320686, 319782, 318881, 317982 ] | 15 => #[ 317085, 316191, 315299, 314409, 313521, 312636, 311753, 310872, 309993, 309116, 308242, 307369, 306499, 305630, 304764, 303900, 303038, 302177, 301319, 300463, 317889, 317012, 316135, 315260, 314386, 313514, 312642, 311772, 310903, 310036, 309169, 308304 ] | 16 => #[ 307440, 306578, 305717, 304857, 303998, 303140, 302284, 301429, 300575, 299723, 298871, 298021, 297172, 296325, 295479, 294634, 293790, 292947, 292106, 291266, 290427, 289589, 288753, 287917, 287083, 286251, 285419, 284589, 283760, 282932, 282105, 281280 ] | 17 => #[ 280456, 279633, 278811, 277990, 277171, 276353, 275536, 274720, 273906, 273093, 272280, 271470, 270660, 269851, 269044, 268238, 267433, 266630, 265827, 265026, 264226, 263427, 262629, 261832, 261037, 260243, 259450, 258658, 257867, 257078, 256290, 255503 ] | 18 => #[ 254717, 253932, 253148, 252366, 251585, 250805, 250026, 249248, 248471, 247696, 246922, 246149, 245377, 244606, 243836, 243068, 242300, 241534, 240769, 240005, 239242, 238481, 237720, 236961, 236203, 235446, 234690, 233935, 233181, 232429, 231677, 230927 ] | 19 => #[ 230178, 229430, 228683, 227937, 227192, 226449, 225706, 224965, 224225, 223485, 222747, 222010, 221275, 220540, 219806, 219074, 218342, 217612, 216883, 216155, 215428, 214702, 213977, 213253, 212530, 211809, 211088, 210369, 209650, 208933, 208217, 207501 ] | 20 => #[ 206787, 206074, 205362, 204651, 203941, 203233, 202525, 201818, 201113, 200408, 199704, 199002, 198300, 197600, 196901, 196202, 195505, 194809, 194114, 193419, 192726, 192034, 191343, 190653, 189964, 189276, 188589, 187903, 187218, 186534, 185851, 185169 ] | 21 => #[ 184488, 183808, 183129, 182451, 181774, 181098, 180423, 179749, 179076, 178404, 177733, 177063, 176394, 175726, 175059, 174393, 173728, 173064, 172401, 171738, 171077, 170417, 169757, 169099, 168441, 167785, 167129, 166475, 165821, 165169, 164517, 163866 ] | 22 => #[ 163216, 162567, 161919, 161272, 160626, 159981, 159336, 158693, 158050, 157409, 156768, 156128, 155490, 154852, 154215, 153579, 152943, 152309, 151676, 151043, 150411, 149781, 149151, 148522, 147894, 147267, 146640, 146015, 145390, 144766, 144144, 143522 ] | 23 => #[ 142900, 142280, 141661, 141042, 140424, 139808, 139191, 138576, 137962, 137348, 136736, 136124, 135513, 134903, 134293, 133685, 133077, 132470, 131864, 131259, 130654, 130051, 129448, 128846, 128245, 127644, 127045, 126446, 125848, 125250, 124654, 124058 ] | 24 => #[ 123463, 122869, 122276, 121683, 121091, 120500, 119910, 119320, 118731, 118143, 117556, 116969, 116384, 115798, 115214, 114631, 114048, 113466, 112884, 112303, 111723, 111144, 110566, 109988, 109411, 108834, 108259, 107684, 107109, 106536, 105963, 105391 ] | 25 => #[ 104819, 104248, 103678, 103109, 102540, 101972, 101404, 100838, 100272, 99706, 99141, 98577, 98014, 97451, 96889, 96327, 95766, 95206, 94646, 94087, 93529, 92971, 92414, 91857, 91302, 90746, 90192, 89638, 89084, 88531, 87979, 87427 ] | 26 => #[ 86876, 86326, 85776, 85226, 84678, 84130, 83582, 83035, 82488, 81943, 81397, 80852, 80308, 79765, 79221, 78679, 78137, 77595, 77054, 76514, 75974, 75435, 74896, 74357, 73819, 73282, 72745, 72209, 71673, 71138, 70603, 70069 ] | 27 => #[ 69535, 69002, 68469, 67936, 67404, 66873, 66342, 65811, 65281, 64752, 64223, 63694, 63166, 62638, 62111, 61584, 61057, 60531, 60005, 59480, 58955, 58431, 57907, 57384, 56861, 56338, 55815, 55294, 54772, 54251, 53730, 53210 ] | 28 => #[ 52690, 52170, 51651, 51132, 50614, 50095, 49578, 49060, 48543, 48026, 47510, 46994, 46478, 45963, 45448, 44933, 44419, 43905, 43391, 42878, 42365, 41852, 41339, 40827, 40315, 39803, 39292, 38781, 38270, 37760, 37250, 36740 ] | 29 => #[ 36230, 35721, 35211, 34703, 34194, 33686, 33177, 32669, 32162, 31654, 31147, 30640, 30133, 29627, 29121, 28615, 28109, 27603, 27097, 26592, 26087, 25582, 25077, 24573, 24069, 23564, 23060, 22557, 22053, 21549, 21046, 20543 ] | 30 => #[ 20040, 19537, 19034, 18532, 18029, 17527, 17025, 16523, 16021, 15519, 15017, 14516, 14014, 13513, 13011, 12510, 12009, 11508, 11007, 10506, 10005, 9505, 9004, 8504, 8003, 7503, 7002, 6502, 6002, 5501, 5001, 4501 ] | 31 => #[ 4001, 3501, 3001, 2501, 2001, 1501, 1001, 501 ] | _ => #[]
def highKernelFast reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The kernel magnitude entry at index i read from the cached blocks: entry i mod 32 of block ⌊i/32⌋ for i < 1000, and the original table's value for i ≥ 1000.
Definition (Lean source)
parameters
i :
ℕ
def
highKernelFast i :
ℕ
given by
if i < 1000 then (highKernelBlock (i / 32)).getD (i % 32) 0 else prawitzKernelMagnitudeIndex i
def highCellInteger reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The integer high-frequency cell for parameter cell j and frequency index i is the ceiling of the integer fraction 6·M·den(r)·15!·d¹⁵ over 25·num(r)·N. Here r is the left endpoint of the parameter cell, M the block-lookup kernel magnitude entry at i, d the high-cell exponent denominator and N the integer Taylor numerator at the high-cell exponent numerator and d. It is the integer-arithmetic form of the rational high cell bound multiplied by one hundred million and rounded up.
Definition (Lean source)
parameters
j i :
ℕ
def
highCellInteger j i :
ℤ
given by
highCeil (6 * (highKernelFast i : ℤ) * r.den * (1307674368000 * d ^ 15)) (25 * r.num * highTaylorNum n d)
def highIntSuffix reviewed
⚑ flagged
Causalean.Stat.CLT.BerryEsseen
The integer suffix sum for parameter cell j and length n ≤ 1000 is the sum of the integer high-frequency cells at the top n grid indices, 1000 − n through 999; it is zero for n = 0.
Definition (Lean source)
parameters
j :
ℕ
def
highIntSuffix j :
ℕ → ℤ