OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorBlocks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LowSpaceSubsetSum.SeparatorBlocks.Block line 15
2. def OAI.LowSpaceSubsetSum.SeparatorBlocks.depth line 22
3. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.transport_sorted line 24
4. def OAI.LowSpaceSubsetSum.SeparatorBlocks.ofFamily line 32

   Source documentation

   Family tables are computed once, then captured by the lookup functions. The runtime interval loop only indexes these stored arrays.

   def ofFamily {g : ℕ} (family : Array (Finset (Fin g)))
       (mask₁ : α → Finset (Fin g)) (mask₂ : β → Finset (Fin g)) : Block α β :=
   …

   Mentions: OAI.LowSpaceSubsetSum.SeparatorBlocks.Block

5. def OAI.LowSpaceSubsetSum.SeparatorBlocks.PairGood line 48
6. def OAI.LowSpaceSubsetSum.SeparatorBlocks.check line 51
7. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.correct line 60
8. def OAI.LowSpaceSubsetSum.SeparatorBlocks.chargeLeft line 89
9. def OAI.LowSpaceSubsetSum.SeparatorBlocks.chargeRight line 93
10. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.sum_charge line 97
11. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.scans_le line 107
12. def OAI.LowSpaceSubsetSum.SeparatorBlocks.peakBound line 133
13. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.peak_le line 136
14. def OAI.LowSpaceSubsetSum.SeparatorBlocks.capacityPeak line 151
15. theorem OAI.LowSpaceSubsetSum.SeparatorBlocks.peak_capacity line 154