OAI/Combinatorics/Progressions/Estimates/AllocatedMaskedFactorBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_normalized line 33
  2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_normalized_factor line 46
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_enlarge line 68
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_smallBox line 89
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedPhysicalSite_normalized line 105
  6. abbrev OAI.Erdos3.VectorPolynomial.MaskedSiteResidueIndex line 144
  7. def OAI.Erdos3.VectorPolynomial.mixedCoveredSiteResidueIntegers line 147
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_ambient_factor line 159
  9. theorem OAI.Erdos3.bufferedCoordinateProjection_lipschitz_uniform line 239
  10. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredSiteResidueLabels_card line 253
  11. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredSiteResidueLabels_card_le_exp line 261