OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationScheduleTrial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete bucket experiment reaches YES in the full residue loop

  1. def OAI.LowSpaceSubsetSum.RepresentationSetup.ScheduleAccepted line 14
  2. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.scheduleAccepted_of_bucket line 20
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_joint_acceptance_probability line 35

    Source documentation

    Retain representation success so its deterministic spread test can also be used when bounding the full prefix execution.

    theorem schedule_joint_acceptance_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

  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_acceptance_probability line 56

    Source documentation

    The experiment reaches its designated lifted bucket in the full counter loop.

    theorem schedule_acceptance_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