OAI/Computability/QuantumFactoring/TableFavorableCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.tableBadCountNet line 21
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableBadCountNet_value line 24
  3. def OAI.ExactQuantumFactoring.BitArithmetic.tableFavorableCountNet line 45

    Source documentation

    The exact source F, computed from supplied prime rows using polynomial integer circuits. Distinctness tests remove repeated table entries.

    def tableFavorableCountNet {k n : ℕ} (m : BooleanNetwork k n) (ps : List (BooleanNetwork k n)) :
    BooleanNetwork k n := natSubOn (primesPhiNet m ps) (tableBadCountNet m ps)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.natSubOn, OAI.ExactQuantumFactoring.BitArithmetic.primesPhiNet, OAI.ExactQuantumFactoring.BitArithmetic.tableBadCountNet

  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableFavorableCountNet_value line 48
  5. def OAI.ExactQuantumFactoring.BitArithmetic.tableBadCountBound line 60
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableBadCountNet_count line 63
  7. def OAI.ExactQuantumFactoring.BitArithmetic.tableFavorableCountBound line 72
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableFavorableCountNet_count line 75