OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationScanTrial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.RepresentationSetup.trialScans line 16
2. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketTrial_resource_failure line 22
3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketTrial_scan_failure line 45

   Source documentation

   One conditional Markov estimate suffices for all buckets and all prefix checks using the same sampled separator families.

   theorem bucketTrial_scan_failure (hn : 20000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000) (B : ℕ) :
       (R.bucketTrialLaw (by omega)).probability (fun h =>
         R.AllocatedResourceGood hn hlog h.1.1 ∧
           R.separatorScanBudget < (R.trialScans hn hlog B h : ℝ)) ≤
         (1 / 10 : ℝ) / (inputScale R.input : ℝ) ^ 100 := by
   …

   Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale

4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_joint_acceptance_with_scan_budget line 72

   Source documentation

   The concrete schedule still succeeds while retaining the resource event and respecting the scan watchdog threshold. Other operation charges can be combined with this event separately.

   theorem schedule_joint_acceptance_with_scan_budget (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

5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_acceptance_with_scan_budget line 124