MaxLeafFormal.RSCover21

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

import MaxLeafFormal.RSCheck

/-!
# RS closed-form rate: cover 3, chunk 21 (generated)

Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
73 intervals covering [27/50, 4/5] for the target 3901/5000.
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 `27/50`. -/
def cover21 : List ℚ := [
  q 221197 409600,
  q 22121 40960,
  q 221223 409600,
  q 55309 102400,
  q 221249 409600,
  q 110631 204800,
  q 8851 16384,
  q 27661 51200,
  q 110657 204800,
  q 11067 20480,
  q 110683 204800,
  q 13837 25600,
  q 110709 204800,
  q 55361 102400,
  q 22147 40960,
  q 27687 51200,
  q 55387 102400,
  q 277 512,
  q 55413 102400,
  q 27713 51200,
  q 55439 102400,
  q 13863 25600,
  q 11093 20480,
  q 27739 51200,
  q 3469 6400,
  q 5553 10240,
  q 13889 25600,
  q 27791 51200,
  q 6951 12800,
  q 27817 51200,
  q 2783 5120,
  q 1741 3200,
  q 13941 25600,
  q 6977 12800,
  q 13967 25600,
  q 699 1280,
  q 13993 25600,
  q 7003 12800,
  q 14019 25600,
  q 877 1600,
  q 7029 12800,
  q 3521 6400,
  q 1411 2560,
  q 1767 3200,
  q 7081 12800,
  q 3547 6400,
  q 7107 12800,
  q 89 160,
  q 3573 6400,
  q 1793 3200,
  q 3599 6400,
  q 903 1600,
  q 145 256,
  q 1819 3200,
  q 229 400,
  q 369 640,
  q 929 1600,
  q 1871 3200,
  q 471 800,
  q 1897 3200,
  q 191 320,
  q 121 200,
  q 981 1600,
  q 497 800,
  q 1007 1600,
  q 51 80,
  q 523 800,
  q 67 100,
  q 549 800,
  q 281 400,
  q 147 200,
  q 307 400,
  q 4 5
]

theorem cover21_ok :
    checkCover (q 3901 5000) (q 4 5) (q 27 50) cover21 = true := by
  decide +kernel

theorem cover21_sound : ∀ σ ∈ Set.Icc (((q 27 50) : ℚ) : ℝ) (((q 4 5) : ℚ) : ℝ),
    rsF σ ≤ (((q 3901 5000) : ℚ) : ℝ) :=
  checkCover_sound cover21_ok

end MaxLeafFormal.RSRate