OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SingleEdgeWeight.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.single_edge_weight line 15
  2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.singletonIsTagged line 23
  3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.singletonTokenWeight line 27
  4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.singletonTokenWeight_nonneg line 32
  5. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.free_center_tree_mean line 40
  6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixedTreeWeight line 61
  7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixedTreeWeight_nonneg line 64
  8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixed_tree_mean line 68
  9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordPrime_le_charged_local line 83
  10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.no_tree_mean_le_one line 91
  11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.IsCollision line 100
  12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.backgroundExponent line 103
  13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.outsideTreeBound line 106
  14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.outsideTreeBound_nonneg line 111
  15. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.outside_tree_mean line 116