OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DivisorPathFilling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathFilling line 21
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathFilling.weight line 24
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathFilling.weight_nonneg line 26
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathFilling.decode line 28
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorPathFilling.sum_weight line 31
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.encode line 40
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.decode_encode line 45
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ShortCorruptSelection.weight_encode line 48
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ManyShortCorrupted line 56
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.nearCorruptMass line 59
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.nearCorruptMass_le_templateMass line 62
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.nearCorruptSum line 82
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.nearCorruptSum_le_mass line 87
14. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.nearCorruptSum_bound line 101