OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorStoredSpace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

All-outcome storage of sampled families and incidence lists

  1. def OAI.LowSpaceSubsetSum.SeparatorStoredMasks.storage line 21

    Source documentation

    Eight arrays of incidence lists, their headers, and the four sampled families with each local mask represented by its indexed bits.

    def storage (families : Fin 4 → Array (Finset (Fin g))) : ℕ :=
…
  2. theorem OAI.LowSpaceSubsetSum.SeparatorStoredMasks.storage_le line 27
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.separator_table_rate_le_capacity line 65
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.sampled_separator_storage line 72