OAI/Combinatorics/Progressions/Estimates/AllocatedAnchoredRecoveredSource.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedPhysicalRankReadCertificate line 28
2. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalRankReadCertificate_of_event_read line 40
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedPhysicalRankReadCertificate.modulusBad_congr line 65
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedPhysicalRankReadCertificate.primeBad_congr line 104
5. theorem OAI.Erdos3.VectorPolynomial.selectedResidueDensityPMF_certifiedRead_badProduct_congr line 115
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedPhysical_recovered_sample_read line 166
7. def OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise line 251
8. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_noise line 258
9. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_deck line 264
10. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_projection line 270
11. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_chart line 276
12. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedAnchored_recovered_sample_read line 283
13. def OAI.Erdos3.VectorPolynomial.AllocatedCenteredRecoveredSampleReadAt line 342
14. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCentered_recovered_sample_read line 374
15. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCentered_recovered_sample_reads line 399
16. def OAI.Erdos3.VectorPolynomial.allocatedAnchoredRecoveredSample line 442
17. def OAI.Erdos3.VectorPolynomial.allocatedAnchoredRecoveredRead line 448
18. theorem OAI.Erdos3.VectorPolynomial.allocatedAnchoredRecoveredSource_spec line 454