OAI/Combinatorics/Progressions/Dynamics/AllocatedReferenceIdealBudget.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.physicalIdealSmoothingLog line 16
  2. def OAI.Erdos3.physicalIdealTailLog line 20
  3. theorem OAI.Erdos3.physicalIdealSmoothingLog_nonneg line 26
  4. theorem OAI.Erdos3.physicalIdealTailLog_nonneg line 34
  5. theorem OAI.Erdos3.physicalIdeal_smoothing_inverse_le_exp line 44
  6. theorem OAI.Erdos3.physicalIdeal_tail_inverse_le_exp line 55
  7. def OAI.Erdos3.VectorPolynomial.allocatedErrorPrimitiveLog line 79
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedErrorPrimitiveLog_bounds line 83
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedErrorPrimitive_constants line 103
  10. def OAI.Erdos3.VectorPolynomial.allocatedProfileGainLog line 160
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileGainLog_nonneg line 163
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileGain_le_exp line 176
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileError_mass_budget line 197
  14. def OAI.Erdos3.VectorPolynomial.allocatedSiteErrorPrimitiveLog line 239
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteErrorPrimitiveLog_bounds line 243
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteErrorPrimitive_constants line 265
  17. def OAI.Erdos3.VectorPolynomial.profileReferenceErrorLog line 322
  18. def OAI.Erdos3.VectorPolynomial.profileReferenceAccuracy line 325
  19. theorem OAI.Erdos3.VectorPolynomial.profileReferenceAccuracy_bounds line 328
  20. theorem OAI.Erdos3.VectorPolynomial.profileReferenceAccuracy_normalized_error line 336
  21. theorem OAI.Erdos3.VectorPolynomial.exists_profileReferenceErrorLog_bound line 357
  22. def OAI.Erdos3.VectorPolynomial.allocatedReferenceIdealError line 381
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceIdealError_nonneg line 385
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceIdealError_add_mask line 392
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceIdealError_share line 398
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceIdealLength_mesh line 404
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceIdealSmoothing_eq line 424