OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SubtreeUnionWeightNonneg.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.subtreeUnionWeight_nonneg line 16
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.subtreeUnionWeight_empty line 25
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.activity_nonneg line 28
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.activity_mean line 31
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.charged_local_le line 36
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordPrime line 44
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordPrime_nonneg line 48
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.recordPrime_le_activity line 56
9. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixed_lit_tree_mean line 71
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.core_primeFactor_zero_of_unlit line 81
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.center_empty_lit_pointwise line 88
12. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixed_unlit_tree_mean line 123