OAI/Combinatorics/Progressions/Estimates/AllocatedZeroLayerDetectorReturn.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.scalarWidths_pos_empty_layers line 37
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.scalarMass_pos_empty_layers line 46
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.nativeDetection_iff_scalarReference_empty_layers line 52
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.scalarAxesWidths_pos_empty_layers line 77
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.scalarAxesMass_pos_empty_layers line 86
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.nativeDetection_to_scalarAxes_empty_layers line 93
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.nativeDetection_from_scalarAxes_empty_layers line 114
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.scalarAxesMass_pos_zero_layers line 165
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.nativeDetection_of_emptyTag_scalarReference line 172