OAI/NumberTheory/OrdinaryCorrelations/HighTrace/RepeatedUnlitTotalEqFixed.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.repeatedUnlitTotal_eq_fixed line 22
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.unlitTailSum line 42
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.unlitPrefactor line 46
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.unlit_tail_sum_bound line 49