OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TreeOccurrences.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.treeOccurrences line 15
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.litEdges line 18
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.edgeVertices line 21
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.edgeVertices_subset line 24
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.lit_vertex_active line 33
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NoComponentTop line 42
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.isolatedCharge line 47
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.isolatedCharge_nonneg line 52
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.incoming_charge_le_isolated line 57
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.incoming_charges_le_vertices line 76
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.subtreeUnionWeight line 100
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tree_norm_charges_le line 103
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.charged_prime_le_tree line 152
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.occurrence_abs_le_lit_amplitude line 183
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.occurrence_product_le line 200
16. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.charged_prime_le_weight line 211