OAI/Combinatorics/Progressions/Estimates/AllocatedOriginalCommonResources.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedConstructedSpatialCoefficient_coarse_bound line 60
  2. theorem OAI.Erdos3.VectorPolynomial.genuineCube_rescale_coefficient_bound line 149
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedGenuineCubeCoefficient_pre_bound line 209
  4. theorem OAI.Erdos3.VectorPolynomial.genuineCube_rescale_joint_coefficient_bound line 286
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedGenuineCubeCoefficient_coarse_bound line 348
  6. def OAI.Erdos3.VectorPolynomial.AllocatedCoarseFamilyResources line 476
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCoarseFamilyResources_of_bounds line 509
  8. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalGenuineResourcesData line 591
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalTrim_bounds line 782
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSampling_bounds line 790
  11. def OAI.Erdos3.VectorPolynomial.allocatedCanonicalCubeThreshold line 807
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalCubeThreshold_bounds line 810
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalGenuineResourcesData_of_coarse line 856
  14. theorem OAI.Erdos3.VectorPolynomial.exists_original_common_genuine_resource_source line 1018