MaxLeafFormal.RSCover17
Source file MaxLeafFormal/RSCover17.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 17 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [550369/1310720, 69131/163840] 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 `550369/1310720`. -/
def cover17 : List ℚ := [
q 137593 327680,
q 110075 262144,
q 275189 655360,
q 550381 1310720,
q 34399 81920,
q 550387 1310720,
q 55039 131072,
q 550393 1310720,
q 137599 327680,
q 550399 1310720,
q 275201 655360,
q 110081 262144,
q 68801 163840,
q 550411 1310720,
q 275207 655360,
q 550417 1310720,
q 27521 65536,
q 550423 1310720,
q 275213 655360,
q 550429 1310720,
q 17201 40960,
q 110087 262144,
q 275219 655360,
q 550441 1310720,
q 137611 327680,
q 550447 1310720,
q 55045 131072,
q 550453 1310720,
q 68807 163840,
q 550459 1310720,
q 275231 655360,
q 110093 262144,
q 137617 327680,
q 550471 1310720,
q 275237 655360,
q 550477 1310720,
q 6881 16384,
q 550483 1310720,
q 275243 655360,
q 550489 1310720,
q 137623 327680,
q 110099 262144,
q 275249 655360,
q 550501 1310720,
q 68813 163840,
q 550507 1310720,
q 55051 131072,
q 550513 1310720,
q 137629 327680,
q 550519 1310720,
q 275261 655360,
q 110105 262144,
q 4301 10240,
q 550531 1310720,
q 275267 655360,
q 550537 1310720,
q 27527 65536,
q 550543 1310720,
q 275273 655360,
q 550549 1310720,
q 68819 163840,
q 110111 262144,
q 275279 655360,
q 550561 1310720,
q 137641 327680,
q 550567 1310720,
q 55057 131072,
q 550573 1310720,
q 34411 81920,
q 550579 1310720,
q 275291 655360,
q 110117 262144,
q 137647 327680,
q 550591 1310720,
q 275297 655360,
q 550597 1310720,
q 13765 32768,
q 550603 1310720,
q 275303 655360,
q 550609 1310720,
q 137653 327680,
q 110123 262144,
q 275309 655360,
q 550621 1310720,
q 17207 40960,
q 550627 1310720,
q 55063 131072,
q 550633 1310720,
q 137659 327680,
q 550639 1310720,
q 275321 655360,
q 110129 262144,
q 68831 163840,
q 550651 1310720,
q 275327 655360,
q 550657 1310720,
q 27533 65536,
q 550663 1310720,
q 275333 655360,
q 550669 1310720,
q 34417 81920,
q 110135 262144,
q 275339 655360,
q 550681 1310720,
q 137671 327680,
q 550687 1310720,
q 55069 131072,
q 550693 1310720,
q 68837 163840,
q 550699 1310720,
q 275351 655360,
q 110141 262144,
q 137677 327680,
q 550711 1310720,
q 275357 655360,
q 550717 1310720,
q 1721 4096,
q 550723 1310720,
q 275363 655360,
q 550729 1310720,
q 137683 327680,
q 110147 262144,
q 275369 655360,
q 550741 1310720,
q 68843 163840,
q 550747 1310720,
q 55075 131072,
q 550753 1310720,
q 137689 327680,
q 550759 1310720,
q 275381 655360,
q 110153 262144,
q 34423 81920,
q 550771 1310720,
q 275387 655360,
q 550777 1310720,
q 27539 65536,
q 550783 1310720,
q 275393 655360,
q 550789 1310720,
q 68849 163840,
q 110159 262144,
q 275399 655360,
q 550801 1310720,
q 137701 327680,
q 550807 1310720,
q 55081 131072,
q 550813 1310720,
q 17213 40960,
q 550819 1310720,
q 275411 655360,
q 110165 262144,
q 137707 327680,
q 550831 1310720,
q 275417 655360,
q 550837 1310720,
q 13771 32768,
q 550843 1310720,
q 275423 655360,
q 550849 1310720,
q 137713 327680,
q 110171 262144,
q 275429 655360,
q 550861 1310720,
q 34429 81920,
q 550867 1310720,
q 55087 131072,
q 550873 1310720,
q 137719 327680,
q 550879 1310720,
q 275441 655360,
q 110177 262144,
q 68861 163840,
q 550891 1310720,
q 275447 655360,
q 550897 1310720,
q 27545 65536,
q 550903 1310720,
q 275453 655360,
q 550909 1310720,
q 269 640,
q 110183 262144,
q 275459 655360,
q 550921 1310720,
q 137731 327680,
q 550927 1310720,
q 55093 131072,
q 550933 1310720,
q 68867 163840,
q 275471 655360,
q 137737 327680,
q 275477 655360,
q 6887 16384,
q 275483 655360,
q 137743 327680,
q 275489 655360,
q 68873 163840,
q 55099 131072,
q 137749 327680,
q 275501 655360,
q 17219 40960,
q 275507 655360,
q 27551 65536,
q 275513 655360,
q 68879 163840,
q 275519 655360,
q 137761 327680,
q 55105 131072,
q 34441 81920,
q 275531 655360,
q 137767 327680,
q 275537 655360,
q 13777 32768,
q 275543 655360,
q 137773 327680,
q 275549 655360,
q 8611 20480,
q 55111 131072,
q 137779 327680,
q 275561 655360,
q 68891 163840,
q 275567 655360,
q 27557 65536,
q 275573 655360,
q 34447 81920,
q 275579 655360,
q 137791 327680,
q 55117 131072,
q 68897 163840,
q 275591 655360,
q 137797 327680,
q 275597 655360,
q 3445 8192,
q 275603 655360,
q 137803 327680,
q 275609 655360,
q 68903 163840,
q 55123 131072,
q 137809 327680,
q 275621 655360,
q 34453 81920,
q 275627 655360,
q 27563 65536,
q 275633 655360,
q 68909 163840,
q 275639 655360,
q 137821 327680,
q 55129 131072,
q 4307 10240,
q 275651 655360,
q 137827 327680,
q 275657 655360,
q 13783 32768,
q 275663 655360,
q 137833 327680,
q 275669 655360,
q 34459 81920,
q 55135 131072,
q 137839 327680,
q 275681 655360,
q 68921 163840,
q 275687 655360,
q 27569 65536,
q 275693 655360,
q 17231 40960,
q 275699 655360,
q 137851 327680,
q 55141 131072,
q 68927 163840,
q 275711 655360,
q 137857 327680,
q 275717 655360,
q 6893 16384,
q 275723 655360,
q 137863 327680,
q 275729 655360,
q 68933 163840,
q 55147 131072,
q 137869 327680,
q 275741 655360,
q 8617 20480,
q 275747 655360,
q 27575 65536,
q 275753 655360,
q 68939 163840,
q 275759 655360,
q 137881 327680,
q 55153 131072,
q 34471 81920,
q 275771 655360,
q 137887 327680,
q 275777 655360,
q 13789 32768,
q 275783 655360,
q 137893 327680,
q 275789 655360,
q 17237 40960,
q 55159 131072,
q 137899 327680,
q 275801 655360,
q 68951 163840,
q 275807 655360,
q 27581 65536,
q 275813 655360,
q 34477 81920,
q 275819 655360,
q 137911 327680,
q 55165 131072,
q 68957 163840,
q 275831 655360,
q 137917 327680,
q 275837 655360,
q 431 1024,
q 275843 655360,
q 137923 327680,
q 275849 655360,
q 68963 163840,
q 55171 131072,
q 137929 327680,
q 275861 655360,
q 34483 81920,
q 275867 655360,
q 27587 65536,
q 275873 655360,
q 68969 163840,
q 275879 655360,
q 137941 327680,
q 55177 131072,
q 17243 40960,
q 275891 655360,
q 137947 327680,
q 275897 655360,
q 13795 32768,
q 275903 655360,
q 137953 327680,
q 275909 655360,
q 34489 81920,
q 55183 131072,
q 137959 327680,
q 275921 655360,
q 68981 163840,
q 275927 655360,
q 27593 65536,
q 275933 655360,
q 8623 20480,
q 275939 655360,
q 137971 327680,
q 55189 131072,
q 68987 163840,
q 275951 655360,
q 137977 327680,
q 275957 655360,
q 6899 16384,
q 275963 655360,
q 137983 327680,
q 275969 655360,
q 68993 163840,
q 55195 131072,
q 137989 327680,
q 275981 655360,
q 17249 40960,
q 275987 655360,
q 27599 65536,
q 275993 655360,
q 68999 163840,
q 275999 655360,
q 138001 327680,
q 55201 131072,
q 34501 81920,
q 276011 655360,
q 138007 327680,
q 276017 655360,
q 13801 32768,
q 276023 655360,
q 138013 327680,
q 276029 655360,
q 4313 10240,
q 55207 131072,
q 138019 327680,
q 276041 655360,
q 69011 163840,
q 276047 655360,
q 27605 65536,
q 276053 655360,
q 34507 81920,
q 276059 655360,
q 138031 327680,
q 55213 131072,
q 69017 163840,
q 276071 655360,
q 138037 327680,
q 276077 655360,
q 3451 8192,
q 276083 655360,
q 138043 327680,
q 276089 655360,
q 69023 163840,
q 55219 131072,
q 138049 327680,
q 276101 655360,
q 34513 81920,
q 276107 655360,
q 27611 65536,
q 276113 655360,
q 69029 163840,
q 276119 655360,
q 138061 327680,
q 55225 131072,
q 8629 20480,
q 276131 655360,
q 138067 327680,
q 276137 655360,
q 13807 32768,
q 276143 655360,
q 138073 327680,
q 276149 655360,
q 34519 81920,
q 55231 131072,
q 138079 327680,
q 276161 655360,
q 69041 163840,
q 276167 655360,
q 27617 65536,
q 276173 655360,
q 17261 40960,
q 276179 655360,
q 138091 327680,
q 55237 131072,
q 69047 163840,
q 276191 655360,
q 138097 327680,
q 276197 655360,
q 6905 16384,
q 276203 655360,
q 138103 327680,
q 276209 655360,
q 69053 163840,
q 55243 131072,
q 138109 327680,
q 276221 655360,
q 1079 2560,
q 276227 655360,
q 27623 65536,
q 276233 655360,
q 69059 163840,
q 276239 655360,
q 138121 327680,
q 55249 131072,
q 34531 81920,
q 276251 655360,
q 138127 327680,
q 276257 655360,
q 13813 32768,
q 276263 655360,
q 138133 327680,
q 276269 655360,
q 17267 40960,
q 55255 131072,
q 138139 327680,
q 69071 163840,
q 27629 65536,
q 34537 81920,
q 138151 327680,
q 69077 163840,
q 138157 327680,
q 1727 4096,
q 138163 327680,
q 69083 163840,
q 138169 327680,
q 34543 81920,
q 27635 65536,
q 69089 163840,
q 138181 327680,
q 17273 40960,
q 138187 327680,
q 13819 32768,
q 138193 327680,
q 34549 81920,
q 138199 327680,
q 69101 163840,
q 27641 65536,
q 4319 10240,
q 138211 327680,
q 69107 163840,
q 138217 327680,
q 6911 16384,
q 138223 327680,
q 69113 163840,
q 138229 327680,
q 17279 40960,
q 27647 65536,
q 69119 163840,
q 138241 327680,
q 34561 81920,
q 138247 327680,
q 13825 32768,
q 138253 327680,
q 8641 20480,
q 138259 327680,
q 69131 163840
]
theorem cover17_ok :
checkCover (q 8030906143 10000000000) (q 69131 163840) (q 550369 1310720) cover17 = true := by
decide +kernel
theorem cover17_sound : ∀ σ ∈ Set.Icc (((q 550369 1310720) : ℚ) : ℝ) (((q 69131 163840) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover17_ok
end MaxLeafFormal.RSRate