OAI/Combinatorics/LowSpaceSubsetSum/Storage/CanonicalMixers.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed input-index mixers

The three disjoint mixer domains are chosen uniformly for every input length; their definition does not inspect the weights or a designated solution.

  1. def OAI.LowSpaceSubsetSum.canonicalMixers line 14
  2. theorem OAI.LowSpaceSubsetSum.canonicalMixers_card line 17
  3. theorem OAI.LowSpaceSubsetSum.canonicalMixers_disjoint line 24
  4. def OAI.LowSpaceSubsetSum.canonicalRepresentationData line 39
  5. def OAI.LowSpaceSubsetSum.canonicalRepresentationSetup line 46

    Source documentation

    The solution is supplied only to the analysis of the fixed runtime data.

    def canonicalRepresentationSetup {n : ℕ} (I : Instance n) (S : Finset (Fin n))
    (hS : weight (fun i => (I.values i : ℤ)) S = I.target) : RepresentationSetup n where
…

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.RepresentationSetup

  6. theorem OAI.LowSpaceSubsetSum.canonicalRepresentationSetup_runtimeData line 55