OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FixedCharges.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixedCharges line 15
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeCoreCharges line 18
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixedCharges_nonneg line 21
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeCoreCharges_nonneg line 24
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.splitCutoff_le line 27
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.localWithList_core_nonneg line 40
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixed_charged_product line 45
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.freeCore_charged_mean line 51
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fixed_group_charged_mean_le line 71
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.assignedKernelIntegral_le_prime_means line 93