OAI/Combinatorics/Progressions/Estimates/AllocatedShortDependence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerArrayJetImage line 13
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerImage_support line 42
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerImage_weighted_inversion line 50
  4. def OAI.Erdos3.VectorPolynomial.allocatedLayerShortIntegerImageAxis line 71
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerShortIntegerImageAxis_exact line 77
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerShortIntegerImageAxis_log_bounds line 84
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_moderate_tail_zero line 124
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_moderate_eval line 139
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_moderate_eval_congr line 152
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_moderateJet_congr line 170
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerModerateIntegerImage_freeze line 201
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_inactive_eval line 244
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_inactive_eval_congr line 269
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_inactiveJet_congr line 284
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerShortIntegerImage_freeze line 312