OAI/Combinatorics/Progressions/Estimates/ConstantCenterUniformLifts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.subtractConstant line 13
  2. theorem OAI.Erdos3.VectorPolynomial.coefficients_subtractConstant line 16
  3. theorem OAI.Erdos3.VectorPolynomial.eval_subtractConstant line 21
  4. theorem OAI.Erdos3.VectorPolynomial.substitute_subtractConstant line 25
  5. theorem OAI.Erdos3.VectorPolynomial.DegreeLE.subtractConstant line 30
  6. theorem OAI.Erdos3.VectorPolynomial.coefficients_subtractConstant_mem line 39
  7. theorem OAI.Erdos3.VectorPolynomial.homogeneousPart_subtractConstant line 48
  8. theorem OAI.Erdos3.VectorPolynomial.hasLayerSamplingRank_subtractConstant_iff line 64
  9. theorem OAI.Erdos3.VectorPolynomial.AffinePolynomialLiftProperties.of_subtractConstant line 79
  10. theorem OAI.Erdos3.VectorPolynomial.HasQuarterAffinePolynomialLifts.of_subtractConstant line 91
  11. theorem OAI.Erdos3.VectorPolynomial.centeredAffineCoefficientTorus_zero line 111
  12. theorem OAI.Erdos3.VectorPolynomial.selectedPhysicalDensity_quarter_lifts line 130
  13. theorem OAI.Erdos3.VectorPolynomial.affineSampleCoefficientArray_subtractConstant line 157
  14. theorem OAI.Erdos3.VectorPolynomial.affineSampleCoefficientTorus_subtractConstant line 172
  15. theorem OAI.Erdos3.VectorPolynomial.selectedPhysicalDensity_subtractConstant line 190
  16. theorem OAI.Erdos3.VectorPolynomial.exists_constant_center_uniform_lifts line 221