OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionBoundedTrial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.CompressionData.AcceptedWithCompactTests line 13
2. theorem OAI.LowSpaceSubsetSum.CompressionData.compact_acceptance_probability line 18

   Source documentation

   Keep the actual seven compact-list tests in the successful event; later resource bounds can use them without an independence premise.

   theorem compact_acceptance_probability (B : ℕ) (hn : 168000000 ≤ n)
       (hsolve : Solvable D.input)
       (hmean : (153 / 20000 : ℝ) * n ≤
         meanDeficiency D.weights Finset.univ (compressionHalfSize n))
       (hlog : Real.logb 2 (inputScale D.input) ≤ (n : ℝ) / 1000000000) :
       (1 / 4 : ℝ) ≤ (D.trialLaw hn).probability (D.AcceptedWithCompactTests B) := by
   …

   Mentions: OAI.LowSpaceSubsetSum.Solvable, OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.compressionHalfSize, OAI.LowSpaceSubsetSum.inputScale

3. theorem OAI.LowSpaceSubsetSum.CompressionData.bounded_compact_acceptance_probability line 31
4. theorem OAI.LowSpaceSubsetSum.CompressionData.bounded_compression_acceptance_probability line 46
5. theorem OAI.LowSpaceSubsetSum.CompressionData.sampled_acceptance_sound line 65