OAI/Combinatorics/Progressions/Geometry/SpatialNumericEnvelopeFunctoriality.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.anisotropicSpatialMeshLog line 13
  2. theorem OAI.Erdos3.anisotropicSpatialMeshThreshold_le_exp line 16
  3. theorem OAI.Erdos3.anisotropicSpatialDensityLip_le_exp line 57
  4. theorem OAI.Erdos3.probabilityProfileLipschitz_le_comparisonProfileBound line 93
  5. def OAI.Erdos3.spatialFixedProfileEnvelope line 97
  6. def OAI.Erdos3.spatialDisplacementEnvelope line 100
  7. def OAI.Erdos3.spatialDiscretizationEnvelope line 103
  8. def OAI.Erdos3.spatialMeshEnvelope line 107
  9. def OAI.Erdos3.spatialLipschitzEnvelope line 110
  10. theorem OAI.Erdos3.spatialCostEnvelopes_nonneg line 113
  11. theorem OAI.Erdos3.spatialProfileLog_le_fixedEnvelope line 121
  12. theorem OAI.Erdos3.spatialDisplacementLog_le_envelope line 132
  13. theorem OAI.Erdos3.spatialDiscretizationLog_le_envelope line 141
  14. theorem OAI.Erdos3.anisotropicSpatialMeshLog_le_envelope line 149
  15. def OAI.Erdos3.spatialLipschitzCostEnvelope line 167
  16. def OAI.Erdos3.spatialThresholdEnvelope line 170
  17. def OAI.Erdos3.spatialBoundaryEnvelope line 173
  18. def OAI.Erdos3.spatialMovementEnvelope line 176
  19. theorem OAI.Erdos3.spatialAuxiliaryDimensions line 178
  20. theorem OAI.Erdos3.spatialPrimitiveCost_bounds line 191
  21. def OAI.Erdos3.normalizedTupleTolerance line 293
  22. def OAI.Erdos3.normalizedTupleNarrowWidth line 297
  23. def OAI.Erdos3.normalizedTupleRadius line 301
  24. def OAI.Erdos3.normalizedTupleResolution line 306
  25. theorem OAI.Erdos3.normalizedTupleNarrowWidth_pos line 317
  26. theorem OAI.Erdos3.normalizedTupleSpatialChoices line 324
  27. theorem OAI.Erdos3.canonicalSlicedSpatialChoices line 372
  28. def OAI.Erdos3.spatialTupleCoarseMesh line 429
  29. theorem OAI.Erdos3.spatialTupleCoarseMesh_spec line 432
  30. theorem OAI.Erdos3.twoTermErrorWidth_budget_antitone line 461
  31. theorem OAI.Erdos3.normalizedTupleRadius_le_coarse line 468
  32. theorem OAI.Erdos3.normalizedTupleCoarseMesh_budget line 480
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedTupleSpatialError_mono_width line 504
  34. theorem OAI.Erdos3.sharedWidthNormalizedTupleSpatialChoices line 532
  35. def OAI.Erdos3.spatialPrimitiveEnvelope line 579
  36. def OAI.Erdos3.spatialParameterBudget line 585
  37. theorem OAI.Erdos3.spatialPrimitiveEnvelope_bounds line 589
  38. theorem OAI.Erdos3.spatialParameterBudget_bounds line 620
  39. theorem OAI.Erdos3.exists_spatialParameterBudget_bound line 631
  40. theorem OAI.Erdos3.map_coefficientErrorSpatialLog line 669
  41. theorem OAI.Erdos3.map_spatialPrimitiveEnvelope line 674
  42. theorem OAI.Erdos3.map_spatialTupleToleranceLog line 682
  43. theorem OAI.Erdos3.map_spatialParameterBudget line 686
  44. theorem OAI.Erdos3.coefficientErrorSpatialLog_mono line 693
  45. theorem OAI.Erdos3.spatialPrimitiveEnvelope_mono line 701
  46. theorem OAI.Erdos3.spatialTupleToleranceLog_mono line 713
  47. theorem OAI.Erdos3.spatialParameterBudget_mono line 719