OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TokenSlot.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TokenSlot line 22
  2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.slotShape line 26
  3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.slotCore line 28
  4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.unorderedEdgeProduct line 30
  5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.unorderedBins line 34
  6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.slotEdgeProduct_named line 39
  7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.pivotBinIndicator_nonneg line 57
  8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.unorderedBins_gate line 65
  9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.token_constants_product line 77
  10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.slot_mass_product line 86
  11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.token_gated_sum line 94
  12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.token_mass_algebra line 110
  13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenNamedSum line 118
  14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenMassProduct line 124
  15. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tokenFactorialProduct line 127
  16. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.unorderedTokenSum line 130
  17. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NamedTokenBound line 138
  18. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrimeNamedBound line 146
  19. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.namedTokenBound_of_prime line 155
  20. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_token_named_sum line 166
  21. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.UnorderedTokenBound line 172
  22. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.unorderedTokenBound_of_named line 181
  23. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_unordered_prime_sum line 202