OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationBoundedTrial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bounded_favorable_trial_probability line 16

   Source documentation

   The finite bounded sampler retains enough probability for the manuscript's round amplification, including the concrete full-execution work events.

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