OAI/Combinatorics/Progressions/Lattices/AllocatedAffineScaleEnvelope.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineReferenceCoefficientLog line 9
  2. theorem OAI.Erdos3.affineReferenceCoefficient_bounds line 12
  3. theorem OAI.Erdos3.affineReferenceError_accuracy line 111
  4. theorem OAI.Erdos3.affineReferenceError_accuracy_separated line 141
  5. def OAI.Erdos3.VectorPolynomial.allocatedAffineL1Log line 181
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineL1_primitive_bounds line 191
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedAffineL1Log_bound line 249
  8. def OAI.Erdos3.VectorPolynomial.allocatedAffineCoefficientAccuracyLog line 291
  9. def OAI.Erdos3.VectorPolynomial.allocatedAffineReferenceAccuracyLog line 295
  10. def OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog line 299
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineL1Log_nonneg line 304
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_bounds line 312
  13. def OAI.Erdos3.VectorPolynomial.allocatedAffineScale line 343
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineScale_lower line 348
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineScale_upper line 354
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLength_ready line 377
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions.active_tuples line 401
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLength_slice_ready line 409
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_kernel_bound line 457
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLength_kernel_ready line 484
  21. def OAI.Erdos3.VectorPolynomial.allocatedAffineScalePolynomial line 501
  22. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedAffineScaleLog_bound line 508