MaxLeafFormal.RSCover11
Source file MaxLeafFormal/RSCover11.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 11 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [876175/2097152, 876475/2097152] 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 `876175/2097152`. -/
def cover11 : List ℚ := [
q 2190439 5242880,
q 4380881 10485760,
q 1095221 2621440,
q 4380887 10485760,
q 438089 1048576,
q 4380893 10485760,
q 136903 327680,
q 4380899 10485760,
q 2190451 5242880,
q 876181 2097152,
q 1095227 2621440,
q 4380911 10485760,
q 2190457 5242880,
q 4380917 10485760,
q 109523 262144,
q 4380923 10485760,
q 2190463 5242880,
q 4380929 10485760,
q 1095233 2621440,
q 876187 2097152,
q 2190469 5242880,
q 4380941 10485760,
q 273809 655360,
q 4380947 10485760,
q 438095 1048576,
q 4380953 10485760,
q 1095239 2621440,
q 4380959 10485760,
q 2190481 5242880,
q 876193 2097152,
q 547621 1310720,
q 4380971 10485760,
q 2190487 5242880,
q 4380977 10485760,
q 219049 524288,
q 4380983 10485760,
q 2190493 5242880,
q 4380989 10485760,
q 68453 163840,
q 876199 2097152,
q 2190499 5242880,
q 4381001 10485760,
q 1095251 2621440,
q 4381007 10485760,
q 438101 1048576,
q 4381013 10485760,
q 547627 1310720,
q 4381019 10485760,
q 2190511 5242880,
q 876205 2097152,
q 1095257 2621440,
q 4381031 10485760,
q 2190517 5242880,
q 4381037 10485760,
q 54763 131072,
q 4381043 10485760,
q 2190523 5242880,
q 4381049 10485760,
q 1095263 2621440,
q 876211 2097152,
q 2190529 5242880,
q 4381061 10485760,
q 547633 1310720,
q 4381067 10485760,
q 438107 1048576,
q 4381073 10485760,
q 1095269 2621440,
q 4381079 10485760,
q 2190541 5242880,
q 876217 2097152,
q 136909 327680,
q 4381091 10485760,
q 2190547 5242880,
q 4381097 10485760,
q 219055 524288,
q 4381103 10485760,
q 2190553 5242880,
q 4381109 10485760,
q 547639 1310720,
q 876223 2097152,
q 2190559 5242880,
q 4381121 10485760,
q 1095281 2621440,
q 4381127 10485760,
q 438113 1048576,
q 4381133 10485760,
q 273821 655360,
q 4381139 10485760,
q 2190571 5242880,
q 876229 2097152,
q 1095287 2621440,
q 4381151 10485760,
q 2190577 5242880,
q 4381157 10485760,
q 109529 262144,
q 4381163 10485760,
q 2190583 5242880,
q 4381169 10485760,
q 1095293 2621440,
q 876235 2097152,
q 2190589 5242880,
q 4381181 10485760,
q 8557 20480,
q 4381187 10485760,
q 438119 1048576,
q 4381193 10485760,
q 1095299 2621440,
q 4381199 10485760,
q 2190601 5242880,
q 876241 2097152,
q 547651 1310720,
q 4381211 10485760,
q 2190607 5242880,
q 4381217 10485760,
q 219061 524288,
q 4381223 10485760,
q 2190613 5242880,
q 4381229 10485760,
q 273827 655360,
q 876247 2097152,
q 2190619 5242880,
q 4381241 10485760,
q 1095311 2621440,
q 4381247 10485760,
q 438125 1048576,
q 4381253 10485760,
q 547657 1310720,
q 4381259 10485760,
q 2190631 5242880,
q 876253 2097152,
q 1095317 2621440,
q 4381271 10485760,
q 2190637 5242880,
q 4381277 10485760,
q 27383 65536,
q 4381283 10485760,
q 2190643 5242880,
q 4381289 10485760,
q 1095323 2621440,
q 876259 2097152,
q 2190649 5242880,
q 4381301 10485760,
q 547663 1310720,
q 4381307 10485760,
q 438131 1048576,
q 4381313 10485760,
q 1095329 2621440,
q 4381319 10485760,
q 2190661 5242880,
q 876265 2097152,
q 273833 655360,
q 4381331 10485760,
q 2190667 5242880,
q 4381337 10485760,
q 219067 524288,
q 4381343 10485760,
q 2190673 5242880,
q 4381349 10485760,
q 547669 1310720,
q 876271 2097152,
q 2190679 5242880,
q 4381361 10485760,
q 1095341 2621440,
q 4381367 10485760,
q 438137 1048576,
q 4381373 10485760,
q 68459 163840,
q 4381379 10485760,
q 2190691 5242880,
q 876277 2097152,
q 1095347 2621440,
q 4381391 10485760,
q 2190697 5242880,
q 4381397 10485760,
q 109535 262144,
q 4381403 10485760,
q 2190703 5242880,
q 4381409 10485760,
q 1095353 2621440,
q 876283 2097152,
q 2190709 5242880,
q 4381421 10485760,
q 273839 655360,
q 4381427 10485760,
q 438143 1048576,
q 4381433 10485760,
q 1095359 2621440,
q 4381439 10485760,
q 2190721 5242880,
q 876289 2097152,
q 547681 1310720,
q 4381451 10485760,
q 2190727 5242880,
q 4381457 10485760,
q 219073 524288,
q 4381463 10485760,
q 2190733 5242880,
q 4381469 10485760,
q 136921 327680,
q 876295 2097152,
q 2190739 5242880,
q 4381481 10485760,
q 1095371 2621440,
q 4381487 10485760,
q 438149 1048576,
q 4381493 10485760,
q 547687 1310720,
q 4381499 10485760,
q 2190751 5242880,
q 876301 2097152,
q 1095377 2621440,
q 4381511 10485760,
q 2190757 5242880,
q 4381517 10485760,
q 54769 131072,
q 4381523 10485760,
q 2190763 5242880,
q 4381529 10485760,
q 1095383 2621440,
q 876307 2097152,
q 2190769 5242880,
q 4381541 10485760,
q 547693 1310720,
q 4381547 10485760,
q 438155 1048576,
q 4381553 10485760,
q 1095389 2621440,
q 4381559 10485760,
q 2190781 5242880,
q 876313 2097152,
q 34231 81920,
q 4381571 10485760,
q 2190787 5242880,
q 4381577 10485760,
q 219079 524288,
q 4381583 10485760,
q 2190793 5242880,
q 4381589 10485760,
q 547699 1310720,
q 876319 2097152,
q 2190799 5242880,
q 4381601 10485760,
q 1095401 2621440,
q 4381607 10485760,
q 438161 1048576,
q 4381613 10485760,
q 273851 655360,
q 4381619 10485760,
q 2190811 5242880,
q 876325 2097152,
q 1095407 2621440,
q 4381631 10485760,
q 2190817 5242880,
q 4381637 10485760,
q 109541 262144,
q 4381643 10485760,
q 2190823 5242880,
q 4381649 10485760,
q 1095413 2621440,
q 876331 2097152,
q 2190829 5242880,
q 4381661 10485760,
q 136927 327680,
q 4381667 10485760,
q 438167 1048576,
q 4381673 10485760,
q 1095419 2621440,
q 4381679 10485760,
q 2190841 5242880,
q 876337 2097152,
q 547711 1310720,
q 4381691 10485760,
q 2190847 5242880,
q 4381697 10485760,
q 219085 524288,
q 4381703 10485760,
q 2190853 5242880,
q 4381709 10485760,
q 273857 655360,
q 876343 2097152,
q 2190859 5242880,
q 4381721 10485760,
q 1095431 2621440,
q 4381727 10485760,
q 438173 1048576,
q 4381733 10485760,
q 547717 1310720,
q 4381739 10485760,
q 2190871 5242880,
q 876349 2097152,
q 1095437 2621440,
q 4381751 10485760,
q 2190877 5242880,
q 4381757 10485760,
q 13693 32768,
q 4381763 10485760,
q 2190883 5242880,
q 4381769 10485760,
q 1095443 2621440,
q 876355 2097152,
q 2190889 5242880,
q 4381781 10485760,
q 547723 1310720,
q 4381787 10485760,
q 438179 1048576,
q 4381793 10485760,
q 1095449 2621440,
q 4381799 10485760,
q 2190901 5242880,
q 876361 2097152,
q 273863 655360,
q 4381811 10485760,
q 2190907 5242880,
q 4381817 10485760,
q 219091 524288,
q 4381823 10485760,
q 2190913 5242880,
q 4381829 10485760,
q 547729 1310720,
q 876367 2097152,
q 2190919 5242880,
q 4381841 10485760,
q 1095461 2621440,
q 4381847 10485760,
q 438185 1048576,
q 4381853 10485760,
q 136933 327680,
q 4381859 10485760,
q 2190931 5242880,
q 876373 2097152,
q 1095467 2621440,
q 4381871 10485760,
q 2190937 5242880,
q 4381877 10485760,
q 109547 262144,
q 4381883 10485760,
q 2190943 5242880,
q 4381889 10485760,
q 1095473 2621440,
q 876379 2097152,
q 2190949 5242880,
q 4381901 10485760,
q 273869 655360,
q 4381907 10485760,
q 438191 1048576,
q 4381913 10485760,
q 1095479 2621440,
q 4381919 10485760,
q 2190961 5242880,
q 876385 2097152,
q 547741 1310720,
q 4381931 10485760,
q 2190967 5242880,
q 4381937 10485760,
q 219097 524288,
q 4381943 10485760,
q 2190973 5242880,
q 4381949 10485760,
q 17117 40960,
q 876391 2097152,
q 2190979 5242880,
q 4381961 10485760,
q 1095491 2621440,
q 4381967 10485760,
q 438197 1048576,
q 4381973 10485760,
q 547747 1310720,
q 4381979 10485760,
q 2190991 5242880,
q 876397 2097152,
q 1095497 2621440,
q 4381991 10485760,
q 2190997 5242880,
q 4381997 10485760,
q 54775 131072,
q 4382003 10485760,
q 2191003 5242880,
q 4382009 10485760,
q 1095503 2621440,
q 876403 2097152,
q 2191009 5242880,
q 4382021 10485760,
q 547753 1310720,
q 4382027 10485760,
q 438203 1048576,
q 4382033 10485760,
q 1095509 2621440,
q 4382039 10485760,
q 2191021 5242880,
q 876409 2097152,
q 136939 327680,
q 4382051 10485760,
q 2191027 5242880,
q 4382057 10485760,
q 219103 524288,
q 4382063 10485760,
q 2191033 5242880,
q 4382069 10485760,
q 547759 1310720,
q 876415 2097152,
q 2191039 5242880,
q 4382081 10485760,
q 1095521 2621440,
q 4382087 10485760,
q 438209 1048576,
q 4382093 10485760,
q 273881 655360,
q 4382099 10485760,
q 2191051 5242880,
q 876421 2097152,
q 1095527 2621440,
q 4382111 10485760,
q 2191057 5242880,
q 4382117 10485760,
q 109553 262144,
q 4382123 10485760,
q 2191063 5242880,
q 4382129 10485760,
q 1095533 2621440,
q 876427 2097152,
q 2191069 5242880,
q 4382141 10485760,
q 68471 163840,
q 4382147 10485760,
q 438215 1048576,
q 4382153 10485760,
q 1095539 2621440,
q 4382159 10485760,
q 2191081 5242880,
q 876433 2097152,
q 547771 1310720,
q 4382171 10485760,
q 2191087 5242880,
q 4382177 10485760,
q 219109 524288,
q 4382183 10485760,
q 2191093 5242880,
q 4382189 10485760,
q 273887 655360,
q 876439 2097152,
q 2191099 5242880,
q 4382201 10485760,
q 1095551 2621440,
q 4382207 10485760,
q 438221 1048576,
q 4382213 10485760,
q 547777 1310720,
q 4382219 10485760,
q 2191111 5242880,
q 876445 2097152,
q 1095557 2621440,
q 4382231 10485760,
q 2191117 5242880,
q 4382237 10485760,
q 27389 65536,
q 4382243 10485760,
q 2191123 5242880,
q 4382249 10485760,
q 1095563 2621440,
q 876451 2097152,
q 2191129 5242880,
q 4382261 10485760,
q 547783 1310720,
q 4382267 10485760,
q 438227 1048576,
q 4382273 10485760,
q 1095569 2621440,
q 4382279 10485760,
q 2191141 5242880,
q 876457 2097152,
q 273893 655360,
q 4382291 10485760,
q 2191147 5242880,
q 4382297 10485760,
q 219115 524288,
q 4382303 10485760,
q 2191153 5242880,
q 4382309 10485760,
q 547789 1310720,
q 876463 2097152,
q 2191159 5242880,
q 4382321 10485760,
q 1095581 2621440,
q 4382327 10485760,
q 438233 1048576,
q 4382333 10485760,
q 34237 81920,
q 4382339 10485760,
q 2191171 5242880,
q 876469 2097152,
q 1095587 2621440,
q 4382351 10485760,
q 2191177 5242880,
q 4382357 10485760,
q 109559 262144,
q 4382363 10485760,
q 2191183 5242880,
q 4382369 10485760,
q 1095593 2621440,
q 876475 2097152
]
theorem cover11_ok :
checkCover (q 8030906143 10000000000) (q 876475 2097152) (q 876175 2097152) cover11 = true := by
decide +kernel
theorem cover11_sound : ∀ σ ∈ Set.Icc (((q 876175 2097152) : ℚ) : ℝ) (((q 876475 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover11_ok
end MaxLeafFormal.RSRate