OAI/Combinatorics/Progressions/Estimates/AllocatedCoverLogBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedIdealCoverInputLog line 15
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverInputLog_bounds line 18
  3. def OAI.Erdos3.VectorPolynomial.allocatedIdealCoverPrimitiveLog line 35
  4. def OAI.Erdos3.VectorPolynomial.allocatedIdealCoverPrimitiveRadius line 39
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverPrimitiveRadius_bounds line 42
  6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedIdealCoverPrimitiveLog_bound line 57
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverRadius_inverse_from_dimensions line 71
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverPrimitiveRadius_le line 118
  9. theorem OAI.Erdos3.kernelOutputEnvelope_mono line 142
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedJointLengthEnvelope_mono line 159
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientErrorAccuracyLog_mono line 185
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimension_mono line 193
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealCoverRadius_half_le_physical line 215
  14. def OAI.Erdos3.VectorPolynomial.allocatedSourceCoverRadiusLog line 254
  15. def OAI.Erdos3.VectorPolynomial.allocatedSourceCoverRadius line 257
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSourceCoverRadius_bounds line 260
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSourceCoverRadius_le_charts line 282
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedSourceCoverRadiusLog_mono line 296
  19. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSourceCoverRadiusLog_bound line 305
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedActualProfileFourier_nonneg line 326
  21. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedActualProfileFourier_bound line 334
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalGeometryLog_nonneg line 370
  23. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedOriginalGeometryLog_bound line 378
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSiteFourier_total_bound line 407