OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedRepresentationTrial.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The stopped representation trial on sampled input-only histories

The trial composes table construction with the residue schedule on a sampled history and its coordinate arrays.

  1. abbrev OAI.LowSpaceSubsetSum.RepresentationData.sampledSchedule line 20
  2. def OAI.LowSpaceSubsetSum.RepresentationData.sampledCodes line 26
  3. theorem OAI.LowSpaceSubsetSum.RepresentationData.sampledCodes_size line 30
  4. theorem OAI.LowSpaceSubsetSum.RepresentationData.sampledCodes_decode line 34
  5. def OAI.LowSpaceSubsetSum.RepresentationData.sampledSignMask line 39
  6. theorem OAI.LowSpaceSubsetSum.RepresentationData.sampledSignMask_value line 42
  7. def OAI.LowSpaceSubsetSum.RepresentationData.sampledRows line 46
  8. theorem OAI.LowSpaceSubsetSum.RepresentationData.sampledRows_value line 52
  9. def OAI.LowSpaceSubsetSum.RepresentationData.executeTrial line 59
  10. theorem OAI.LowSpaceSubsetSum.RepresentationData.executeTrial_value line 66
  11. theorem OAI.LowSpaceSubsetSum.RepresentationData.executeTrial_account line 78
  12. theorem OAI.LowSpaceSubsetSum.RepresentationData.executeTrial_accepts_core line 91
  13. def OAI.LowSpaceSubsetSum.RepresentationData.stoppedTrial line 112
  14. theorem OAI.LowSpaceSubsetSum.RepresentationData.stoppedTrial_of_core line 119
  15. theorem OAI.LowSpaceSubsetSum.RepresentationData.stoppedTrial_sound line 126
  16. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bounded_stopped_probability line 149

    Source documentation

    The bounded sampler reaches an actually completed accepting watchdog execution with the same inverse-polynomial lower bound.

    theorem bounded_stopped_probability (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize))
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000) (B : ℕ) :
    let hlog := representation_log_budget (by omega : 10000 ≤ n)
…

    Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.representation_log_budget