OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedAdditiveBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Adding the seven sequential generation stages without inflating exponents

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.Budgeted line 15

    Source documentation

    Each completed stage releases scratch space and retains its bounded seed.

    def Budgeted {S : SamplerCoupling α} {X : Realization w N S}
    (E : Execution X) (B D k : ℕ) : Prop :=
…

    Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.WordSeedMeasured.Execution

  2. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.budgeted_one line 19
  3. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.budgeted_bind line 27
  4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.budgeted_bindSeed line 39