OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationCoreFavorable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Favorable probability for the complete representation core ledger

The event includes task initialization, every reported pair, copied replay state and loop control, in addition to the streamed queries and separator scans. It is defined on the input-only run and original target.

  1. def OAI.LowSpaceSubsetSum.RepresentationData.sampledCoreUnits line 20
  2. def OAI.LowSpaceSubsetSum.RepresentationData.CoreFavorable line 26
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtime_core_favorable_of_favorable line 39
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bounded_runtime_core_probability line 60

    Source documentation

    Bounded sampler exhaustion is charged before transporting the stronger full-core event. No solution enters the runtime algorithm.

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