OAI/NumberTheory/TwoPoint/Bounds/PrimeDegreeCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal degree deletion together with divisibility by a fixed padding divisor. All tests use the common prime coordinates.

  1. def OAI.TwoPointCorrelations.primeSubsetIndex line 15
  2. lemma OAI.TwoPointCorrelations.primeSubsetIndex_value line 20
  3. def OAI.TwoPointCorrelations.primeSiteBits line 26
  4. lemma OAI.TwoPointCorrelations.primeSubsetIndex_bits line 30
  5. lemma OAI.TwoPointCorrelations.primeSiteBits_card line 35
  6. def OAI.TwoPointCorrelations.degreeDivisorCircuit line 39
  7. lemma OAI.TwoPointCorrelations.degreeDivisorCircuit_eval line 45
  8. lemma OAI.TwoPointCorrelations.degreeDivisorCircuit_depth line 58
  9. lemma OAI.TwoPointCorrelations.degreeDivisorCircuit_size line 67
  10. lemma OAI.TwoPointCorrelations.degreeDivisorCircuit_size_exp line 79
  11. lemma OAI.TwoPointCorrelations.prime_divisor_all_bits line 123
  12. lemma OAI.TwoPointCorrelations.degreeDivisorCircuit_integer line 141