OAI/NumberTheory/OrdinaryCorrelations/Elliott/ConstantsA.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphBridge.constants_A line 43
2. lemma OAI.OrdinaryCorrelations.GraphBridge.center_eq_source line 46
3. lemma OAI.OrdinaryCorrelations.GraphBridge.source_primes line 72
4. lemma OAI.OrdinaryCorrelations.GraphBridge.source_core line 76
5. lemma OAI.OrdinaryCorrelations.GraphBridge.source_mean line 78
6. lemma OAI.OrdinaryCorrelations.GraphBridge.source_weight line 81
7. def OAI.OrdinaryCorrelations.GraphBridge.family line 99
8. def OAI.OrdinaryCorrelations.GraphBridge.cuts line 112
9. lemma OAI.OrdinaryCorrelations.GraphBridge.source_core_sum line 127
10. lemma OAI.OrdinaryCorrelations.GraphBridge.cutoffCount_integer line 132
11. lemma OAI.OrdinaryCorrelations.GraphBridge.cut_at_integer line 140
12. lemma OAI.OrdinaryCorrelations.GraphBridge.prime_factor_integer line 155
13. lemma OAI.OrdinaryCorrelations.GraphBridge.edge_at_integer line 202
14. theorem OAI.OrdinaryCorrelations.GraphBridge.centered_graph_bound line 217