OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSeparatorTrial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.separator_coverage_ninety_nine line 11
2. abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.SeparatorDraws line 29
3. def OAI.LowSpaceSubsetSum.RepresentationSetup.separatorLaw line 33
4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosen_separator_coverage line 43

   Source documentation

   Coverage applies to the actual designated indexed masks. Its law is independent after all earlier choices, even though its sizes depend on them.

   theorem chosen_separator_coverage (h : R.PrimeHistory) (r : R.Residues h.2)
       (hn : 10000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
       (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r) :
       (99 / 100 : ℝ) ≤ (R.separatorLaw h (by omega)).probability (fun draws =>
         SeparatorCheck.Covered (SeparatorCheck.sampledFamilies draws)
           ((R.topCoordinates h.1.1.1 h.1.2).encodeEntry (R.chosenEntry h r hn hlog 0))
           ((R.topCoordinates h.1.1.1 h.1.2).encodeEntry (R.chosenEntry h r hn hlog 1))) := by
   …

   Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.SeparatorCheck.Covered, OAI.LowSpaceSubsetSum.SeparatorCheck.sampledFamilies

5. abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.BucketTrialHistory line 69
6. def OAI.LowSpaceSubsetSum.RepresentationSetup.bucketTrialLaw line 72
7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraTrial_modulus_pos line 76
8. def OAI.LowSpaceSubsetSum.RepresentationSetup.BucketAccepted line 82
9. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketTrial_acceptance_probability line 90

   Source documentation

   The actual finite experiment, including its separator families and its prefix search, accepts with inverse-polynomial probability.

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