OAI/Combinatorics/Progressions/Estimates/AllocatedCanonicalSourceExistence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedCanonicalGenuineData line 34
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalGenuineData_of_resources line 246
  3. theorem OAI.Erdos3.VectorPolynomial.exists_canonical_common_genuine_source line 380
  4. def OAI.Erdos3.VectorPolynomial.AllocatedUniversalCanonicalSourceAt line 480
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedUniversalCanonicalSourceAt_of_mesh line 524
  6. def OAI.Erdos3.VectorPolynomial.AllocatedFlexibleCanonicalSourceAt line 585
  7. def OAI.Erdos3.VectorPolynomial.AllocatedInitializedCanonicalSourceAt line 637
  8. def OAI.Erdos3.VectorPolynomial.AllocatedInitializedCanonicalSource line 663
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedInitializedCanonicalSourceAt.to_source line 690
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedInitializedCanonicalSource_of_cutoff line 704
  11. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_flexible_canonical_sources line 764
  12. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_initialized_canonical_sources line 845
  13. theorem OAI.Erdos3.VectorPolynomial.exists_initialized_canonical_sources line 924