OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorIncidenceTable.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Stored separator incidence lists and logarithmic interval queries

Each sampled family index occurs once in the stored list, even when two sampled sets are equal. Preprocessing scans indices in increasing order. Interval tests make two bounded binary searches in that stored list; they never scan the family. The counting view is used only in the proofs.

  1. def OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table line 20
  2. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table_mem line 23
  3. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table_length line 34
  4. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table_sorted line 40
  5. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table_monotone line 46
  6. def OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.lower line 58
  7. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.lower_spec line 62
  8. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.lower_bounded line 70
  9. def OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.hit line 73
  10. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.hit_iff line 75
  11. def OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.count line 96
  12. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.hit_count line 99
  13. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.count_split line 104
  14. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.count_zero_of_not_hit line 130
  15. def OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.preprocess line 139

    Source documentation

    Both compatibility modes are stored for every local bit mask.

    def preprocess (g : ℕ) (family : Array β) (compatible : Fin (2 ^ g) → β → Bool) :
    Array (Array ℕ) := Array.ofFn (table family compatible)

    Mentions: OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.table

  16. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.preprocess_storage line 142
  17. theorem OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.eight_table_capacity line 151

    Source documentation

    Two modes on four blocks have the manuscript's stated flat capacity.

    theorem eight_table_capacity (g : ℕ) (families : Fin 8 → Array β)
    (compatible : Fin 8 → Fin (2 ^ g) → β → Bool)
    (hν : ∀ i, (families i).size ≤ 10 * 2 ^ g + 1) :
    (∑ i : Fin 8, ((preprocess g (families i) (compatible i)).toList.map Array.size).sum) ≤
      8 * 2 ^ g * (10 * 2 ^ g + 1) := by
…

    Mentions: OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.preprocess