MaxLeafFormal.RSCover20

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

import MaxLeafFormal.RSCheck

/-!
# RS closed-form rate: cover 2, chunk 20 (generated)

Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
60 intervals covering [3/20, 31/100] for the target 7807/10000.
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 `3/20`. -/
def cover20 : List ℚ := [
  q 19 100,
  q 21 100,
  q 23 100,
  q 6 25,
  q 1 4,
  q 13 50,
  q 53 200,
  q 27 100,
  q 11 40,
  q 7 25,
  q 113 400,
  q 57 200,
  q 23 80,
  q 29 100,
  q 117 400,
  q 59 200,
  q 237 800,
  q 119 400,
  q 239 800,
  q 3 10,
  q 241 800,
  q 121 400,
  q 97 320,
  q 243 800,
  q 487 1600,
  q 61 200,
  q 489 1600,
  q 49 160,
  q 981 3200,
  q 491 1600,
  q 983 3200,
  q 123 400,
  q 197 640,
  q 493 1600,
  q 1973 6400,
  q 987 3200,
  q 79 256,
  q 247 800,
  q 1977 6400,
  q 989 3200,
  q 3957 12800,
  q 1979 6400,
  q 3959 12800,
  q 99 320,
  q 3961 12800,
  q 1981 6400,
  q 3963 12800,
  q 7927 25600,
  q 991 3200,
  q 7929 25600,
  q 793 2560,
  q 7931 25600,
  q 1983 6400,
  q 7933 25600,
  q 15867 51200,
  q 3967 12800,
  q 15869 51200,
  q 1587 5120,
  q 15871 51200,
  q 31 100
]

theorem cover20_ok :
    checkCover (q 7807 10000) (q 31 100) (q 3 20) cover20 = true := by
  decide +kernel

theorem cover20_sound : ∀ σ ∈ Set.Icc (((q 3 20) : ℚ) : ℝ) (((q 31 100) : ℚ) : ℝ),
    rsF σ ≤ (((q 7807 10000) : ℚ) : ℝ) :=
  checkCover_sound cover20_ok

end MaxLeafFormal.RSRate