OAI/NumberTheory/OrdinaryCorrelations/HighTrace/CylinderBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cylinderBudget line 16
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.coefficient_le_cylinderBudget line 18
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cylinderBudget_nonneg line 23
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cylinderBudget_le_exp line 25
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_cylinder_budget line 60