MaxLeafFormal.RSCover19

Source file MaxLeafFormal/RSCover19.lean of the Lean project (how it is built).

import MaxLeafFormal.RSCheck

/-!
# RS closed-form rate: cover 1, chunk 19 (generated)

Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
93 intervals covering [2281/5120, 4/5] 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 `2281/5120`. -/
def cover19 : List ℚ := [
  q 913 2048,
  q 571 1280,
  q 4571 10240,
  q 2287 5120,
  q 4577 10240,
  q 229 512,
  q 4583 10240,
  q 2293 5120,
  q 4589 10240,
  q 287 640,
  q 919 2048,
  q 2299 5120,
  q 4601 10240,
  q 1151 2560,
  q 4607 10240,
  q 461 1024,
  q 4613 10240,
  q 577 1280,
  q 2311 5120,
  q 1157 2560,
  q 2317 5120,
  q 29 64,
  q 2323 5120,
  q 1163 2560,
  q 2329 5120,
  q 583 1280,
  q 467 1024,
  q 1169 2560,
  q 2341 5120,
  q 293 640,
  q 2347 5120,
  q 235 512,
  q 2353 5120,
  q 589 1280,
  q 2359 5120,
  q 1181 2560,
  q 473 1024,
  q 37 80,
  q 2371 5120,
  q 1187 2560,
  q 2377 5120,
  q 119 256,
  q 1193 2560,
  q 299 640,
  q 1199 2560,
  q 601 1280,
  q 241 512,
  q 151 320,
  q 1211 2560,
  q 607 1280,
  q 1217 2560,
  q 61 128,
  q 1223 2560,
  q 613 1280,
  q 1229 2560,
  q 77 160,
  q 247 512,
  q 619 1280,
  q 311 640,
  q 125 256,
  q 157 320,
  q 631 1280,
  q 317 640,
  q 637 1280,
  q 1 2,
  q 643 1280,
  q 323 640,
  q 649 1280,
  q 163 320,
  q 131 256,
  q 329 640,
  q 83 160,
  q 67 128,
  q 169 320,
  q 341 640,
  q 43 80,
  q 347 640,
  q 35 64,
  q 353 640,
  q 89 160,
  q 181 320,
  q 23 40,
  q 187 320,
  q 19 32,
  q 193 320,
  q 49 80,
  q 101 160,
  q 13 20,
  q 107 160,
  q 11 16,
  q 29 40,
  q 61 80,
  q 4 5
]

theorem cover19_ok :
    checkCover (q 8030906143 10000000000) (q 4 5) (q 2281 5120) cover19 = true := by
  decide +kernel

theorem cover19_sound : ∀ σ ∈ Set.Icc (((q 2281 5120) : ℚ) : ℝ) (((q 4 5) : ℚ) : ℝ),
    rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
  checkCover_sound cover19_ok

end MaxLeafFormal.RSRate