OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedScheduleLedger.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.taskStarts_positive line 11
2. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.local_queries_le_prefix line 19
3. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.local_copies_le_prefix line 29
4. theorem OAI.LowSpaceSubsetSum.BudgetedScheduleLedger.bucket_units line 47
5. theorem OAI.LowSpaceSubsetSum.BudgetedScheduleLedger.units_sum line 85
6. theorem OAI.LowSpaceSubsetSum.BudgetedScheduleLedger.residue_overhead line 113
7. theorem OAI.LowSpaceSubsetSum.BudgetedScheduleLedger.range_sum_fin line 130
8. theorem OAI.LowSpaceSubsetSum.BudgetedScheduleLedger.allowance_eq line 138
9. theorem OAI.LowSpaceSubsetSum.BudgetedScheduleLedger.allowance_scale line 150

   Source documentation

   Every bucket is paid from the original source ledger. The residue loop itself contributes only a polynomial factor, including early stopping.

   theorem allowance_scale (D : RepresentationScheduleData n g) (F : IndexedMask n)
       (hF : F.semantic = D.signs) (hn : 10000 ≤ n) (B : ℕ)
       (families : Fin 4 → Array (Finset (Fin g))) :
       BudgetedSchedule.allowance D F hF B families ≤
         inputScale D.input ^ 14 * D.coreUnits B families := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RepresentationScheduleData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.BudgetedSchedule.allowance, OAI.LowSpaceSubsetSum.inputScale