import MaxLeafFormal.RSCheck /-! # RS closed-form rate: cover 1, chunk 18 (generated) Generated by `scripts/export_rs_cover.py` (bisection as in `ancillary/rs_closed_form_interval.py`, SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`). 500 intervals covering [69131/163840, 2281/5120] for the target 8030906143/10000000000. Do not edit by hand. The data are not trusted: `decide +kernel` re-checks every interval. -/ set_option maxRecDepth 100000 namespace MaxLeafFormal.RSRate /-- The right ends of the intervals, starting from `69131/163840`. -/ def cover18 : List ℚ := [ q 27653 65536, q 34567 81920, q 138271 327680, q 69137 163840, q 138277 327680, q 3457 8192, q 138283 327680, q 69143 163840, q 138289 327680, q 34573 81920, q 27659 65536, q 69149 163840, q 138301 327680, q 2161 5120, q 138307 327680, q 13831 32768, q 138313 327680, q 34579 81920, q 138319 327680, q 69161 163840, q 27665 65536, q 17291 40960, q 138331 327680, q 69167 163840, q 138337 327680, q 6917 16384, q 138343 327680, q 69173 163840, q 138349 327680, q 8647 20480, q 27671 65536, q 69179 163840, q 138361 327680, q 34591 81920, q 138367 327680, q 13837 32768, q 138373 327680, q 17297 40960, q 138379 327680, q 69191 163840, q 27677 65536, q 34597 81920, q 138391 327680, q 69197 163840, q 138397 327680, q 865 2048, q 138403 327680, q 69203 163840, q 138409 327680, q 34603 81920, q 27683 65536, q 69209 163840, q 138421 327680, q 17303 40960, q 138427 327680, q 13843 32768, q 138433 327680, q 34609 81920, q 138439 327680, q 69221 163840, q 27689 65536, q 8653 20480, q 138451 327680, q 69227 163840, q 138457 327680, q 6923 16384, q 138463 327680, q 69233 163840, q 138469 327680, q 17309 40960, q 27695 65536, q 69239 163840, q 138481 327680, q 34621 81920, q 138487 327680, q 13849 32768, q 138493 327680, q 541 1280, q 138499 327680, q 69251 163840, q 27701 65536, q 34627 81920, q 138511 327680, q 69257 163840, q 138517 327680, q 3463 8192, q 138523 327680, q 69263 163840, q 138529 327680, q 34633 81920, q 27707 65536, q 69269 163840, q 138541 327680, q 8659 20480, q 138547 327680, q 13855 32768, q 138553 327680, q 34639 81920, q 138559 327680, q 69281 163840, q 27713 65536, q 17321 40960, q 138571 327680, q 69287 163840, q 138577 327680, q 6929 16384, q 138583 327680, q 69293 163840, q 138589 327680, q 4331 10240, q 27719 65536, q 69299 163840, q 138601 327680, q 34651 81920, q 138607 327680, q 13861 32768, q 138613 327680, q 17327 40960, q 138619 327680, q 69311 163840, q 27725 65536, q 34657 81920, q 138631 327680, q 69317 163840, q 138637 327680, q 1733 4096, q 138643 327680, q 69323 163840, q 138649 327680, q 34663 81920, q 27731 65536, q 69329 163840, q 138661 327680, q 17333 40960, q 138667 327680, q 13867 32768, q 138673 327680, q 34669 81920, q 138679 327680, q 69341 163840, q 27737 65536, q 2167 5120, q 138691 327680, q 69347 163840, q 138697 327680, q 6935 16384, q 69353 163840, q 17339 40960, q 69359 163840, q 34681 81920, q 13873 32768, q 8671 20480, q 69371 163840, q 34687 81920, q 69377 163840, q 3469 8192, q 69383 163840, q 34693 81920, q 69389 163840, q 4337 10240, q 13879 32768, q 34699 81920, q 69401 163840, q 17351 40960, q 69407 163840, q 6941 16384, q 69413 163840, q 8677 20480, q 69419 163840, q 34711 81920, q 13885 32768, q 17357 40960, q 69431 163840, q 34717 81920, q 69437 163840, q 217 512, q 69443 163840, q 34723 81920, q 69449 163840, q 17363 40960, q 13891 32768, q 34729 81920, q 69461 163840, q 8683 20480, q 69467 163840, q 6947 16384, q 69473 163840, q 17369 40960, q 69479 163840, q 34741 81920, q 13897 32768, q 4343 10240, q 69491 163840, q 34747 81920, q 69497 163840, q 3475 8192, q 69503 163840, q 34753 81920, q 69509 163840, q 8689 20480, q 13903 32768, q 34759 81920, q 69521 163840, q 17381 40960, q 69527 163840, q 6953 16384, q 69533 163840, q 2173 5120, q 69539 163840, q 34771 81920, q 13909 32768, q 17387 40960, q 69551 163840, q 34777 81920, q 69557 163840, q 1739 4096, q 69563 163840, q 34783 81920, q 69569 163840, q 17393 40960, q 13915 32768, q 34789 81920, q 69581 163840, q 4349 10240, q 69587 163840, q 6959 16384, q 69593 163840, q 17399 40960, q 69599 163840, q 34801 81920, q 13921 32768, q 8701 20480, q 69611 163840, q 34807 81920, q 69617 163840, q 3481 8192, q 69623 163840, q 34813 81920, q 69629 163840, q 17 40, q 13927 32768, q 34819 81920, q 69641 163840, q 17411 40960, q 69647 163840, q 6965 16384, q 69653 163840, q 8707 20480, q 69659 163840, q 34831 81920, q 13933 32768, q 17417 40960, q 69671 163840, q 34837 81920, q 69677 163840, q 871 2048, q 69683 163840, q 34843 81920, q 69689 163840, q 17423 40960, q 13939 32768, q 34849 81920, q 69701 163840, q 8713 20480, q 69707 163840, q 6971 16384, q 69713 163840, q 17429 40960, q 69719 163840, q 34861 81920, q 13945 32768, q 2179 5120, q 69731 163840, q 34867 81920, q 69737 163840, q 3487 8192, q 69743 163840, q 34873 81920, q 8719 20480, q 34879 81920, q 17441 40960, q 6977 16384, q 4361 10240, q 34891 81920, q 17447 40960, q 34897 81920, q 1745 4096, q 34903 81920, q 17453 40960, q 34909 81920, q 1091 2560, q 6983 16384, q 17459 40960, q 34921 81920, q 8731 20480, q 34927 81920, q 3493 8192, q 34933 81920, q 4367 10240, q 34939 81920, q 17471 40960, q 6989 16384, q 8737 20480, q 34951 81920, q 17477 40960, q 34957 81920, q 437 1024, q 34963 81920, q 17483 40960, q 34969 81920, q 8743 20480, q 6995 16384, q 17489 40960, q 34981 81920, q 4373 10240, q 34987 81920, q 3499 8192, q 34993 81920, q 8749 20480, q 34999 81920, q 17501 40960, q 7001 16384, q 547 1280, q 35011 81920, q 17507 40960, q 35017 81920, q 1751 4096, q 35023 81920, q 17513 40960, q 35029 81920, q 4379 10240, q 7007 16384, q 17519 40960, q 35041 81920, q 8761 20480, q 35047 81920, q 3505 8192, q 35053 81920, q 2191 5120, q 35059 81920, q 17531 40960, q 7013 16384, q 8767 20480, q 35071 81920, q 17537 40960, q 35077 81920, q 877 2048, q 35083 81920, q 17543 40960, q 35089 81920, q 8773 20480, q 7019 16384, q 17549 40960, q 35101 81920, q 1097 2560, q 35107 81920, q 3511 8192, q 35113 81920, q 8779 20480, q 35119 81920, q 17561 40960, q 7025 16384, q 4391 10240, q 35131 81920, q 17567 40960, q 35137 81920, q 1757 4096, q 35143 81920, q 17573 40960, q 35149 81920, q 2197 5120, q 17579 40960, q 8791 20480, q 3517 8192, q 4397 10240, q 17591 40960, q 8797 20480, q 17597 40960, q 55 128, q 17603 40960, q 8803 20480, q 17609 40960, q 4403 10240, q 3523 8192, q 8809 20480, q 17621 40960, q 2203 5120, q 17627 40960, q 1763 4096, q 17633 40960, q 4409 10240, q 17639 40960, q 8821 20480, q 3529 8192, q 1103 2560, q 17651 40960, q 8827 20480, q 17657 40960, q 883 2048, q 17663 40960, q 8833 20480, q 17669 40960, q 2209 5120, q 3535 8192, q 8839 20480, q 17681 40960, q 4421 10240, q 17687 40960, q 1769 4096, q 17693 40960, q 553 1280, q 17699 40960, q 8851 20480, q 3541 8192, q 4427 10240, q 17711 40960, q 8857 20480, q 17717 40960, q 443 1024, q 17723 40960, q 8863 20480, q 17729 40960, q 4433 10240, q 3547 8192, q 8869 20480, q 17741 40960, q 1109 2560, q 17747 40960, q 1775 4096, q 17753 40960, q 4439 10240, q 17759 40960, q 8881 20480, q 3553 8192, q 2221 5120, q 17771 40960, q 8887 20480, q 889 2048, q 8893 20480, q 139 320, q 8899 20480, q 4451 10240, q 1781 4096, q 2227 5120, q 8911 20480, q 4457 10240, q 8917 20480, q 223 512, q 8923 20480, q 4463 10240, q 8929 20480, q 2233 5120, q 1787 4096, q 4469 10240, q 8941 20480, q 559 1280, q 8947 20480, q 895 2048, q 8953 20480, q 2239 5120, q 8959 20480, q 4481 10240, q 1793 4096, q 1121 2560, q 8971 20480, q 4487 10240, q 8977 20480, q 449 1024, q 8983 20480, q 4493 10240, q 8989 20480, q 281 640, q 1799 4096, q 4499 10240, q 9001 20480, q 2251 5120, q 9007 20480, q 901 2048, q 9013 20480, q 1127 2560, q 9019 20480, q 4511 10240, q 1805 4096, q 2257 5120, q 4517 10240, q 113 256, q 4523 10240, q 2263 5120, q 4529 10240, q 1133 2560, q 907 2048, q 2269 5120, q 4541 10240, q 71 160, q 4547 10240, q 455 1024, q 4553 10240, q 1139 2560, q 4559 10240, q 2281 5120 ] theorem cover18_ok : checkCover (q 8030906143 10000000000) (q 2281 5120) (q 69131 163840) cover18 = true := by decide +kernel theorem cover18_sound : ∀ σ ∈ Set.Icc (((q 69131 163840) : ℚ) : ℝ) (((q 2281 5120) : ℚ) : ℝ), rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) := checkCover_sound cover18_ok end MaxLeafFormal.RSRate