MaxLeafFormal.RSCover1
Source file MaxLeafFormal/RSCover1.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 1 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [67601/163840, 272057/655360] 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 `67601/163840`. -/
def cover1 : List ℚ := [
q 27041 65536,
q 16901 40960,
q 135211 327680,
q 67607 163840,
q 135217 327680,
q 6761 16384,
q 135223 327680,
q 67613 163840,
q 135229 327680,
q 2113 5120,
q 27047 65536,
q 67619 163840,
q 135241 327680,
q 33811 81920,
q 135247 327680,
q 13525 32768,
q 135253 327680,
q 16907 40960,
q 135259 327680,
q 67631 163840,
q 27053 65536,
q 33817 81920,
q 135271 327680,
q 67637 163840,
q 135277 327680,
q 1691 4096,
q 135283 327680,
q 67643 163840,
q 135289 327680,
q 33823 81920,
q 27059 65536,
q 67649 163840,
q 135301 327680,
q 16913 40960,
q 135307 327680,
q 13531 32768,
q 135313 327680,
q 33829 81920,
q 135319 327680,
q 67661 163840,
q 27065 65536,
q 4229 10240,
q 135331 327680,
q 67667 163840,
q 135337 327680,
q 6767 16384,
q 135343 327680,
q 67673 163840,
q 135349 327680,
q 16919 40960,
q 27071 65536,
q 67679 163840,
q 135361 327680,
q 33841 81920,
q 135367 327680,
q 13537 32768,
q 135373 327680,
q 8461 20480,
q 135379 327680,
q 67691 163840,
q 27077 65536,
q 33847 81920,
q 135391 327680,
q 67697 163840,
q 135397 327680,
q 3385 8192,
q 135403 327680,
q 67703 163840,
q 135409 327680,
q 33853 81920,
q 27083 65536,
q 67709 163840,
q 135421 327680,
q 529 1280,
q 135427 327680,
q 13543 32768,
q 135433 327680,
q 33859 81920,
q 135439 327680,
q 67721 163840,
q 27089 65536,
q 16931 40960,
q 135451 327680,
q 67727 163840,
q 135457 327680,
q 6773 16384,
q 135463 327680,
q 67733 163840,
q 135469 327680,
q 8467 20480,
q 27095 65536,
q 67739 163840,
q 135481 327680,
q 33871 81920,
q 135487 327680,
q 13549 32768,
q 135493 327680,
q 16937 40960,
q 135499 327680,
q 67751 163840,
q 27101 65536,
q 33877 81920,
q 135511 327680,
q 67757 163840,
q 135517 327680,
q 847 2048,
q 135523 327680,
q 67763 163840,
q 135529 327680,
q 33883 81920,
q 27107 65536,
q 271073 655360,
q 67769 163840,
q 271079 655360,
q 135541 327680,
q 54217 131072,
q 16943 40960,
q 271091 655360,
q 135547 327680,
q 271097 655360,
q 13555 32768,
q 271103 655360,
q 135553 327680,
q 271109 655360,
q 33889 81920,
q 54223 131072,
q 135559 327680,
q 271121 655360,
q 67781 163840,
q 271127 655360,
q 27113 65536,
q 271133 655360,
q 8473 20480,
q 271139 655360,
q 135571 327680,
q 54229 131072,
q 67787 163840,
q 271151 655360,
q 135577 327680,
q 271157 655360,
q 6779 16384,
q 271163 655360,
q 135583 327680,
q 271169 655360,
q 67793 163840,
q 54235 131072,
q 135589 327680,
q 271181 655360,
q 16949 40960,
q 271187 655360,
q 27119 65536,
q 271193 655360,
q 67799 163840,
q 271199 655360,
q 135601 327680,
q 54241 131072,
q 33901 81920,
q 271211 655360,
q 135607 327680,
q 271217 655360,
q 13561 32768,
q 271223 655360,
q 135613 327680,
q 271229 655360,
q 2119 5120,
q 54247 131072,
q 135619 327680,
q 271241 655360,
q 67811 163840,
q 271247 655360,
q 27125 65536,
q 271253 655360,
q 33907 81920,
q 271259 655360,
q 135631 327680,
q 54253 131072,
q 67817 163840,
q 271271 655360,
q 135637 327680,
q 271277 655360,
q 3391 8192,
q 271283 655360,
q 135643 327680,
q 271289 655360,
q 67823 163840,
q 54259 131072,
q 135649 327680,
q 271301 655360,
q 33913 81920,
q 271307 655360,
q 27131 65536,
q 271313 655360,
q 67829 163840,
q 271319 655360,
q 135661 327680,
q 54265 131072,
q 8479 20480,
q 271331 655360,
q 135667 327680,
q 271337 655360,
q 13567 32768,
q 271343 655360,
q 135673 327680,
q 271349 655360,
q 33919 81920,
q 54271 131072,
q 135679 327680,
q 271361 655360,
q 67841 163840,
q 271367 655360,
q 27137 65536,
q 271373 655360,
q 16961 40960,
q 271379 655360,
q 135691 327680,
q 54277 131072,
q 67847 163840,
q 271391 655360,
q 135697 327680,
q 271397 655360,
q 6785 16384,
q 271403 655360,
q 135703 327680,
q 271409 655360,
q 67853 163840,
q 54283 131072,
q 135709 327680,
q 271421 655360,
q 4241 10240,
q 271427 655360,
q 27143 65536,
q 271433 655360,
q 67859 163840,
q 271439 655360,
q 135721 327680,
q 54289 131072,
q 33931 81920,
q 271451 655360,
q 135727 327680,
q 271457 655360,
q 13573 32768,
q 271463 655360,
q 135733 327680,
q 271469 655360,
q 16967 40960,
q 54295 131072,
q 135739 327680,
q 271481 655360,
q 67871 163840,
q 271487 655360,
q 27149 65536,
q 271493 655360,
q 33937 81920,
q 271499 655360,
q 135751 327680,
q 54301 131072,
q 67877 163840,
q 271511 655360,
q 135757 327680,
q 271517 655360,
q 1697 4096,
q 271523 655360,
q 135763 327680,
q 271529 655360,
q 67883 163840,
q 54307 131072,
q 135769 327680,
q 271541 655360,
q 33943 81920,
q 271547 655360,
q 27155 65536,
q 271553 655360,
q 67889 163840,
q 271559 655360,
q 135781 327680,
q 54313 131072,
q 16973 40960,
q 271571 655360,
q 135787 327680,
q 271577 655360,
q 13579 32768,
q 271583 655360,
q 135793 327680,
q 271589 655360,
q 33949 81920,
q 54319 131072,
q 135799 327680,
q 271601 655360,
q 67901 163840,
q 271607 655360,
q 27161 65536,
q 271613 655360,
q 1061 2560,
q 271619 655360,
q 135811 327680,
q 54325 131072,
q 67907 163840,
q 271631 655360,
q 135817 327680,
q 271637 655360,
q 6791 16384,
q 271643 655360,
q 135823 327680,
q 271649 655360,
q 67913 163840,
q 54331 131072,
q 135829 327680,
q 271661 655360,
q 16979 40960,
q 271667 655360,
q 27167 65536,
q 271673 655360,
q 67919 163840,
q 271679 655360,
q 135841 327680,
q 54337 131072,
q 33961 81920,
q 271691 655360,
q 135847 327680,
q 271697 655360,
q 13585 32768,
q 271703 655360,
q 135853 327680,
q 271709 655360,
q 8491 20480,
q 54343 131072,
q 135859 327680,
q 271721 655360,
q 67931 163840,
q 271727 655360,
q 27173 65536,
q 271733 655360,
q 33967 81920,
q 271739 655360,
q 135871 327680,
q 54349 131072,
q 67937 163840,
q 271751 655360,
q 135877 327680,
q 271757 655360,
q 3397 8192,
q 271763 655360,
q 135883 327680,
q 271769 655360,
q 67943 163840,
q 54355 131072,
q 135889 327680,
q 271781 655360,
q 33973 81920,
q 271787 655360,
q 27179 65536,
q 271793 655360,
q 67949 163840,
q 271799 655360,
q 135901 327680,
q 54361 131072,
q 4247 10240,
q 271811 655360,
q 135907 327680,
q 271817 655360,
q 13591 32768,
q 271823 655360,
q 135913 327680,
q 271829 655360,
q 33979 81920,
q 54367 131072,
q 135919 327680,
q 271841 655360,
q 67961 163840,
q 271847 655360,
q 27185 65536,
q 271853 655360,
q 16991 40960,
q 271859 655360,
q 135931 327680,
q 54373 131072,
q 67967 163840,
q 271871 655360,
q 135937 327680,
q 271877 655360,
q 543757 1310720,
q 6797 16384,
q 543763 1310720,
q 271883 655360,
q 543769 1310720,
q 135943 327680,
q 108755 262144,
q 271889 655360,
q 543781 1310720,
q 67973 163840,
q 543787 1310720,
q 54379 131072,
q 543793 1310720,
q 135949 327680,
q 543799 1310720,
q 271901 655360,
q 108761 262144,
q 8497 20480,
q 543811 1310720,
q 271907 655360,
q 543817 1310720,
q 27191 65536,
q 543823 1310720,
q 271913 655360,
q 543829 1310720,
q 67979 163840,
q 108767 262144,
q 271919 655360,
q 543841 1310720,
q 135961 327680,
q 543847 1310720,
q 54385 131072,
q 543853 1310720,
q 33991 81920,
q 543859 1310720,
q 271931 655360,
q 108773 262144,
q 135967 327680,
q 543871 1310720,
q 271937 655360,
q 543877 1310720,
q 13597 32768,
q 543883 1310720,
q 271943 655360,
q 543889 1310720,
q 135973 327680,
q 108779 262144,
q 271949 655360,
q 543901 1310720,
q 16997 40960,
q 543907 1310720,
q 54391 131072,
q 543913 1310720,
q 135979 327680,
q 543919 1310720,
q 271961 655360,
q 108785 262144,
q 67991 163840,
q 543931 1310720,
q 271967 655360,
q 543937 1310720,
q 27197 65536,
q 543943 1310720,
q 271973 655360,
q 543949 1310720,
q 33997 81920,
q 108791 262144,
q 271979 655360,
q 543961 1310720,
q 135991 327680,
q 543967 1310720,
q 54397 131072,
q 543973 1310720,
q 67997 163840,
q 543979 1310720,
q 271991 655360,
q 108797 262144,
q 135997 327680,
q 543991 1310720,
q 271997 655360,
q 543997 1310720,
q 425 1024,
q 544003 1310720,
q 272003 655360,
q 544009 1310720,
q 136003 327680,
q 108803 262144,
q 272009 655360,
q 544021 1310720,
q 68003 163840,
q 544027 1310720,
q 54403 131072,
q 544033 1310720,
q 136009 327680,
q 544039 1310720,
q 272021 655360,
q 108809 262144,
q 34003 81920,
q 544051 1310720,
q 272027 655360,
q 544057 1310720,
q 27203 65536,
q 544063 1310720,
q 272033 655360,
q 544069 1310720,
q 68009 163840,
q 108815 262144,
q 272039 655360,
q 544081 1310720,
q 136021 327680,
q 544087 1310720,
q 54409 131072,
q 544093 1310720,
q 17003 40960,
q 544099 1310720,
q 272051 655360,
q 108821 262144,
q 136027 327680,
q 544111 1310720,
q 272057 655360
]
theorem cover1_ok :
checkCover (q 8030906143 10000000000) (q 272057 655360) (q 67601 163840) cover1 = true := by
decide +kernel
theorem cover1_sound : ∀ σ ∈ Set.Icc (((q 67601 163840) : ℚ) : ℝ) (((q 272057 655360) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover1_ok
end MaxLeafFormal.RSRate