OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionQueryBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Actual compression join queries across the deterministic residue loop

  1. theorem OAI.LowSpaceSubsetSum.MatchPotential.count_perm line 17
  2. theorem OAI.LowSpaceSubsetSum.CompressionData.groupOutput_perm line 29
  3. def OAI.LowSpaceSubsetSum.CompressionData.leftJoin line 39
  4. def OAI.LowSpaceSubsetSum.CompressionData.rightJoin line 49
  5. theorem OAI.LowSpaceSubsetSum.CompressionData.leftJoin_user line 59
  6. theorem OAI.LowSpaceSubsetSum.CompressionData.rightJoin_user line 64
  7. def OAI.LowSpaceSubsetSum.CompressionData.leftPotential line 69
  8. def OAI.LowSpaceSubsetSum.CompressionData.rightPotential line 73
  9. theorem OAI.LowSpaceSubsetSum.CompressionData.leftJoin_bounds line 78
  10. theorem OAI.LowSpaceSubsetSum.CompressionData.rightJoin_bounds line 100
  11. theorem OAI.LowSpaceSubsetSum.CompressionData.sum_leftPotential line 123
  12. theorem OAI.LowSpaceSubsetSum.CompressionData.sum_rightPotential line 129
  13. def OAI.LowSpaceSubsetSum.CompressionData.residueQueries line 137

    Source documentation

    The query counter of the actually enabled two joins. The right join is skipped on overflow, and all joins are skipped when a compact-list test fails.

    def residueQueries (B : ℕ) (e : Equiv.Perm (Fin n)) (q : CompressionSetup.PrimeSpace n)
    (z : Fin q.val) : ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace

  14. theorem OAI.LowSpaceSubsetSum.CompressionData.residueQueries_le line 145
  15. theorem OAI.LowSpaceSubsetSum.CompressionData.sum_residueQueries_le line 158
  16. theorem OAI.LowSpaceSubsetSum.CompressionData.queries_half_exponential line 169
  17. theorem OAI.LowSpaceSubsetSum.CompressionData.leftJoin_nodes line 201

    Source documentation

    Capacity is respected even at arbitrary stopped control prefixes.

    theorem leftJoin_nodes (B : ℕ) (e : Equiv.Perm (Fin n)) (q : CompressionSetup.PrimeSpace n)
    (z : Fin q.val) (fuel : ℕ) :
    BinaryTrie.nodes (D.leftJoin B e q z fuel).user.tree ≤
      (WeightEncoding.weightWidth D.input + 1) * (compressionDictionaryCapacity n + 1) := by
…

    Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.BinaryTrie.nodes, OAI.LowSpaceSubsetSum.WeightEncoding.weightWidth, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity