OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSamplingLoss.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The bounded sampler's unconditional loss on the main input guard

  1. theorem OAI.LowSpaceSubsetSum.sampler_linear_le_pow line 11
  2. theorem OAI.LowSpaceSubsetSum.sampler_prime_tail line 18
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rangeCallBound_le line 34
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.samplerError_le_pow line 54
  5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryCoupling_failure_pow line 83
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.samplerError_guard line 89

    Source documentation

    The implementation guard makes the coupling error smaller than the polynomial survival margin, without conditioning on sampling success.

    theorem samplerError_guard (hn : 10000 ≤ n)
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000) :
    R.rangeCallBound / (2 : ℝ) ^ (n ^ 3) + 4 * Real.exp (-((n : ℝ) ^ 2 / 4)) ≤
      (1 / 10 : ℝ) / (inputScale R.input : ℝ) ^ 110 := by
…

    Mentions: OAI.LowSpaceSubsetSum.inputScale

  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryCoupling_failure_guard line 111