OAI/NumberTheory/OrdinaryCorrelations/HighTrace/StepFactor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.stepFactor line 15
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeCharge line 20
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeCharge_nonneg line 25
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.theta_div_bounds line 28
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.beta_eq_core line 36
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.beta_eq_center line 39
7. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.charged_return_le_one line 42
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeFactor_split_steps line 76