OAI/Geometry/BallPacking/Annuli/BaseHorizontalForms.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.firstBaseCoefficient line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstBaseCoefficient_smooth line 16
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstBaseCoefficient_fderiv line 20
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstBase_horizontalCoupling line 28
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondBase_horizontalCoupling_isInvertible line 42
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalCoupling_oneCovector_isInvertible line 63
  7. def OAI.PackingSufficiencySupport.Hamiltonian.baseCoefficient line 80
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseCoefficient_smooth line 82
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseCoefficient_fderiv line 85
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseCoefficient_vertical line 91
  11. def OAI.PackingSufficiencySupport.Hamiltonian.weightedSecondCoefficient line 99
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedSecondCoefficient_smooth line 102
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedSecondCoefficient_fderiv line 107
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.weighted_horizontalCoupling_isInvertible line 121
  15. abbrev OAI.PackingSufficiencySupport.Hamiltonian.CircleModel line 141
  16. def OAI.PackingSufficiencySupport.Hamiltonian.circleInclusion line 143
  17. def OAI.PackingSufficiencySupport.Hamiltonian.ambientAngular line 145
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.ambientAngular_apply line 148
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.ambientAngular_smooth line 151
  20. def OAI.PackingSufficiencySupport.Hamiltonian.circleAngular line 156
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_euclidean line 159
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.ambientAngular_chart_smooth line 165
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.circle_coe_smooth line 171
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleAngular_joint_smooth line 176
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleAngular_smooth line 182
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleAngular_closed line 187
  27. def OAI.PackingSufficiencySupport.Hamiltonian.circleTurn line 199
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_smooth line 201
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_deriv line 204
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleAngular_unit_pullback line 210
  31. def OAI.PackingSufficiencySupport.Hamiltonian.shortCircleArgument line 241
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_isOpenMap line 243
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortCircleArgument_turn line 247
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.real_contDiffAt_argument line 259
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortCircleArgument_smooth_at line 267
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_short_slit line 274
  37. def OAI.PackingSufficiencySupport.Hamiltonian.circleBandCoordinate line 286
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleBandCoordinate_apply line 306
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleBandCoordinate_source line 308
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleBand_compact line 311
  41. def OAI.PackingSufficiencySupport.Hamiltonian.intervalClock line 314
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_smooth line 316
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_monotone line 319
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_deriv_nonneg line 323
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_zero line 326
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_one line 329
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_bounds line 332
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_ordered_smooth_clocks line 335
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_shortCircleArgument line 375
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_deriv_smooth line 381
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_deriv_zero_left line 384
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_deriv_zero_right line 391
  53. def OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity line 398
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_support line 401
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_tsupport line 412
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_smooth line 416
  57. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_nonneg line 429
  58. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_turn line 433
  59. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_integral line 438
  60. theorem OAI.PackingSufficiencySupport.Hamiltonian.expNegInvGlue_hasDerivAt line 449
  61. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothTransition_deriv_pos line 453
  62. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_deriv_pos line 472
  63. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_strictMonoOn line 485
  64. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_image line 490
  65. theorem OAI.PackingSufficiencySupport.Hamiltonian.intervalClock_smooth_inverse line 502
  66. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleClockDensity_pos line 520