OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SourceSystem.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceSystem line 17
  2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.rho line 25
  3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceLength line 26
  4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.pathLength line 27
  5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listCutoff line 28
  6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceMinPrime line 29
  7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_prime_lower line 31
  8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceLength_le line 42
  9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.pathLength_le line 46
  10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listCutoff_le line 50
  11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.divisorSlots_le line 57
  12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_lineListSlots_le line 65
  13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceErrorConstant line 86
  14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceErrorBound line 89
  15. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.restorationError_source_bound line 92
  16. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourceErrorBound_tendsto line 119