OAI/Combinatorics/Progressions/Geometry/SpatialChoiceEnvelope.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.smoothSpatialDensityCap_le_exp line 11
  2. theorem OAI.Erdos3.smoothSpatialDensityLip_le_exp line 28
  3. def OAI.Erdos3.spatialGridAccuracy line 62
  4. theorem OAI.Erdos3.spatialGridAccuracy_pos line 64
  5. theorem OAI.Erdos3.spatialGridAccuracy_le line 67
  6. def OAI.Erdos3.smoothSpatialPointAccuracy line 74
  7. theorem OAI.Erdos3.smoothSpatialPointAccuracy_pos line 80
  8. def OAI.Erdos3.smoothJointResolution line 86
  9. def OAI.Erdos3.smoothJointWidth line 91
  10. def OAI.Erdos3.smoothJointRadius line 95
  11. theorem OAI.Erdos3.smoothSpatial_output_choices line 100
  12. theorem OAI.Erdos3.smoothSpatial_grid_tolerance line 120
  13. def OAI.Erdos3.spatialDensityCapLog line 192
  14. def OAI.Erdos3.spatialDensityLipLog line 195
  15. theorem OAI.Erdos3.smoothSpatialDensity_log_bounds line 198
  16. theorem OAI.Erdos3.spatialModulusPower_le_exp line 211
  17. theorem OAI.Erdos3.spatialGridAccuracy_inverse_le_exp line 222
  18. def OAI.Erdos3.spatialPointLog line 236
  19. theorem OAI.Erdos3.smoothSpatialPointAccuracy_inverse_le_exp line 239
  20. def OAI.Erdos3.spatialChoiceLog line 280
  21. theorem OAI.Erdos3.spatialChoiceLog_nonneg line 284
  22. theorem OAI.Erdos3.smoothJointResolution_width_le_exp line 291
  23. theorem OAI.Erdos3.smoothJointRadius_inverse_le_exp line 330
  24. theorem OAI.Erdos3.smoothSpatialOutputScale_le_exp line 361
  25. def OAI.Erdos3.smoothVectorSpatialError line 393
  26. theorem OAI.Erdos3.smoothVectorSpatialError_nonneg line 401
  27. def OAI.Erdos3.VectorPolynomial.allocatedSpatialColumns line 429
  28. def OAI.Erdos3.VectorPolynomial.allocatedSpatialResidueColumns line 433
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialColumns_residue line 441
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialColumns_scaled_bound line 448
  31. def OAI.Erdos3.VectorPolynomial.allocatedSpatialOutputLaw line 461
  32. def OAI.Erdos3.VectorPolynomial.allocatedSpatialProxy line 469
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatial_site_error line 482
  34. theorem OAI.Erdos3.smoothJointParameters_spec line 518
  35. def OAI.Erdos3.spatialChosenHeightLog line 531
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_le_scale line 546
  37. def OAI.Erdos3.VectorPolynomial.allocatedSpatialColumnWidth line 553
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialColumnWidth_nonneg line 557
  39. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialColumnWidth_le_exp line 563
  40. def OAI.Erdos3.VectorPolynomial.allocatedSpatialHeight line 582
  41. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialHeight_spec line 592
  42. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialHeight_pos line 599
  43. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialHeight_one_le line 602
  44. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialHeight_le_exp line 605
  45. def OAI.Erdos3.spatialProfileEnvelope line 623
  46. def OAI.Erdos3.spatialCapEnvelope line 626
  47. def OAI.Erdos3.spatialLipEnvelope line 629
  48. def OAI.Erdos3.spatialPointEnvelope line 632
  49. def OAI.Erdos3.spatialChoiceEnvelope line 635
  50. def OAI.Erdos3.spatialHeightEnvelope line 641
  51. def OAI.Erdos3.spatialRadiusEnvelope line 644
  52. def OAI.Erdos3.spatialParameterEnvelope line 647
  53. theorem OAI.Erdos3.spatialEnvelopes_nonneg line 650
  54. theorem OAI.Erdos3.spatialProfileLog_le_envelope line 659
  55. theorem OAI.Erdos3.spatialCapLog_le_envelope line 667
  56. theorem OAI.Erdos3.spatialLipLog_le_envelope line 674
  57. theorem OAI.Erdos3.spatialPointLog_le_envelope line 682
  58. theorem OAI.Erdos3.spatialChoiceLog_le_envelope line 694
  59. theorem OAI.Erdos3.spatialChosenHeightLog_le_envelope line 710
  60. theorem OAI.Erdos3.spatialRadiusLog_le_envelope line 726