OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FarFilling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarFilling line 19
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarFilling.weight line 22
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarFilling.weight_nonneg line 24
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarFilling.decode line 26
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarFilling.sum_weight line 29
6. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.FarCertificate line 38
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.ManyFarCorrupted line 44
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.farCertificate_exists line 46
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.FarCertificate.encode line 60
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.FarCertificate.decode_encode line 65
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.FarCertificate.weight_encode line 68
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.manyFarMass line 76
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.manyFarMass_le_templateMass line 79
14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.manyFarSum line 97
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.manyFarSum_le_mass line 101
16. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.manyFarSum_bound line 115