OAI/Geometry/CylinderCovering/Results.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.triangularHistorical line 123
  2. theorem OAI.CylinderCovering.ruledHistorical line 128
  3. theorem OAI.CylinderCovering.nilpotentC1 line 131
  4. theorem OAI.CylinderCovering.angularExplicit line 134
  5. theorem OAI.CylinderCovering.ruledProjection line 137
  6. theorem OAI.CylinderCovering.angularCubic line 140
  7. theorem OAI.CylinderCovering.radialAligned line 142
  8. theorem OAI.CylinderCovering.radialActualSweep line 144
  9. theorem OAI.CylinderCovering.regularTriangularCounterexample line 147
  10. theorem OAI.CylinderCovering.simplexProjectionIdentity line 150
  11. theorem OAI.CylinderCovering.angularEndpoint line 153
  12. theorem OAI.CylinderCovering.angularEndpointScaled line 155
  13. theorem OAI.CylinderCovering.Cubic.scaledMain line 158
  14. theorem OAI.CylinderCovering.regularParallelogramCounterexample line 161
  15. theorem OAI.CylinderCovering.regularOpenCounterexample line 164
  16. theorem OAI.CylinderCovering.openParallelogramEnlargement line 167
  17. theorem OAI.CylinderCovering.singularFlexible line 179
  18. theorem OAI.CylinderCovering.cartesianAperture line 181
  19. theorem OAI.CylinderCovering.ruledComparisons line 183
  20. theorem OAI.CylinderCovering.rationalThreshold line 191
  21. theorem OAI.CylinderCovering.orthogonalZeroDiagonal line 194
  22. theorem OAI.CylinderCovering.nilpotentSaving line 197
  23. theorem OAI.CylinderCovering.barycentricProjection line 199
  24. theorem OAI.CylinderCovering.radialSquareRootCap line 202
  25. theorem OAI.CylinderCovering.regularMetricNormalization line 205
  26. theorem OAI.CylinderCovering.angularGeneral line 207
  27. theorem OAI.CylinderCovering.rationalConstruction line 209
  28. theorem OAI.CylinderCovering.nilpotentConstruction line 212
  29. theorem OAI.CylinderCovering.singularEdgeOneDictionary line 214
  30. theorem OAI.CylinderCovering.barycentricCore line 216
  31. theorem OAI.CylinderCovering.localFootprintCertificates line 218
  32. theorem OAI.CylinderCovering.regularAngularExplicit line 220
  33. theorem OAI.CylinderCovering.rationalDictionaryCoefficients line 227
  34. theorem OAI.CylinderCovering.rationalDictionaryExpansion line 229
  35. theorem OAI.CylinderCovering.singularExtensions line 235
  36. theorem OAI.CylinderCovering.unitEdgeTriangular line 237
  37. theorem OAI.CylinderCovering.angularExtensions line 244
  38. theorem OAI.CylinderCovering.nilpotentSmoothRate line 249
  39. theorem OAI.CylinderCovering.shortenedBeamCosts line 254
  40. theorem OAI.CylinderCovering.rationalGlobalInversion line 256
  41. theorem OAI.CylinderCovering.ruledProductLocal line 258
  42. theorem OAI.CylinderCovering.ruledProductCellGeometry line 260
  43. theorem OAI.CylinderCovering.rationalDictionary line 262
  44. theorem OAI.CylinderCovering.beamNeighborhoodAlternative line 269
  45. theorem OAI.CylinderCovering.shortenedBeams line 272
  46. theorem OAI.CylinderCovering.beamNeighborhoodCounterexamples line 274
  47. theorem OAI.CylinderCovering.rationalEquality line 282
  48. theorem OAI.CylinderCovering.physicalFootprintCertificates line 284
  49. theorem OAI.CylinderCovering.canonicalFootprintFinite line 290
  50. theorem OAI.CylinderCovering.halfheightCertificates line 292
  51. theorem OAI.CylinderCovering.physicalCapFinite line 294
  52. theorem OAI.CylinderCovering.absoluteFootprintPolygon line 300
  53. theorem OAI.CylinderCovering.rationalEqualityCover line 302
  54. theorem OAI.CylinderCovering.radialVariants line 304
  55. theorem OAI.CylinderCovering.physicalCoordinateCosts line 310
  56. theorem OAI.CylinderCovering.physicalTriangleConstruction line 312
  57. theorem OAI.CylinderCovering.physicalNormalization line 314
  58. theorem OAI.CylinderCovering.physicalCapNormalized line 316
  59. theorem OAI.CylinderCovering.angularSquaredDirect line 318
  60. theorem OAI.CylinderCovering.radialUniformApproximation line 320
  61. theorem OAI.CylinderCovering.regularBeamNeighborhood line 325
  62. theorem OAI.CylinderCovering.rationalOpenSchedules line 329
  63. theorem OAI.CylinderCovering.regularOpenParallelogram line 331
  64. theorem OAI.CylinderCovering.physicalPaddedFinite line 335
  65. theorem OAI.CylinderCovering.beamProjectionFactor line 337
  66. theorem OAI.CylinderCovering.barycentricEnclosure line 341
  67. theorem OAI.CylinderCovering.nilpotentSmoothRateCertificates line 346
  68. theorem OAI.CylinderCovering.radialOverlapQuantitative line 351
  69. theorem OAI.CylinderCovering.orthonormalHeightCoverage line 353
  70. theorem OAI.CylinderCovering.halfheightGeometry line 355