OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationFavorableTrial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous acceptance, reader work, and separator scan bounds

  1. def OAI.LowSpaceSubsetSum.RepresentationSetup.trialQueries line 14
  2. def OAI.LowSpaceSubsetSum.RepresentationSetup.FavorableTrial line 22

    Source documentation

    These work bounds refer to the entire hypothetical execution, including prefixes and counter iterations skipped after an early YES.

    def FavorableTrial (hn : 20000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (B : ℕ) (h : R.BucketTrialHistory (by omega)) : Prop :=
…

    Mentions: OAI.LowSpaceSubsetSum.mixerSize

  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.favorable_trial_probability line 32