OAI/Combinatorics/Progressions/Estimates/AllocatedGenuineCoverFromRaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.sourceCoverParameter line 12
  2. theorem OAI.Erdos3.sourceCoverParameter_bounds line 17
  3. theorem OAI.Erdos3.sourceCoverParameter_threshold line 34
  4. theorem OAI.Erdos3.sourceCoverParameter_mono line 47
  5. theorem OAI.Erdos3.exists_sourceCoverParameter_bound line 56
  6. def OAI.Erdos3.VectorPolynomial.allocatedCommonCoverParameter line 89
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonCoverThreshold_bound line 110
  8. theorem OAI.Erdos3.VectorPolynomial.allocated_original_exponential_comparison_mesh line 293
  9. theorem OAI.Erdos3.VectorPolynomial.allocated_original_ideal_exponential_comparison line 483
  10. theorem OAI.Erdos3.VectorPolynomial.allocated_original_source_exponential_comparison line 648
  11. def OAI.Erdos3.VectorPolynomial.AllocatedSourceCoverContract line 812
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedSourceCoverContract_of_sampling line 902
  13. theorem OAI.Erdos3.VectorPolynomial.exists_original_common_source_cover line 977
  14. def OAI.Erdos3.VectorPolynomial.AllocatedRawCoverData line 1080
  15. def OAI.Erdos3.VectorPolynomial.AllocatedGenuineCoverData line 1232
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedGenuineCoverData_of_raw line 1402