OAI/NumberTheory/OrdinaryCorrelations/HighTrace/PrimeSystem.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem line 15
  2. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Index line 22
  3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IsCore line 23
  4. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.(instance at line 24) line 24
  5. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Residues line 26
  6. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.CoreIndex line 27
  7. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.CoreResidues line 28
  8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.epsilon line 30
  9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.eta line 31
  10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.kappa line 32
  11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.A line 33
  12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.betaC line 34
  13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.amplitude line 36
  14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.beta line 37
  15. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.harmonicCore line 39
  16. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.shiftCore line 41
  17. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.restrictCore line 43
  18. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cutoffCount line 45
  19. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Cutoffs line 48
  20. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.occurrenceCount line 57
  21. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IsFixed line 60
  22. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FixedIndex line 63
  23. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FreeIndex line 64
  24. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FreeCoreIndex line 65
  25. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FreeCenterIndex line 67
  26. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FixedResidues line 69
  27. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FreeCoreResidues line 71
  28. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FreeCenterResidues line 73
  29. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.splitResidues line 76
  30. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.coreFromSplit line 82
  31. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.restrictCore_merge line 86
  32. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.activity line 96
  33. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.occurrenceFactor line 98
  34. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeFactor line 105
  35. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cutoffProduct line 110
  36. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.kernel line 115
  37. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cutoffProduct_nonneg line 119
  38. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.core_primeFactor_nonneg line 123