OAI/Geometry/BallPacking/Annuli/SurfacePathPositivity.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPrimitive_coupling line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPath_isInvertible line 36
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceInterpolatedLayer_smooth line 55
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceInterpolatedLayer_firstDerivative line 64
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceInterpolatedLayer_firstDerivative_nonneg line 81
  6. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondPrimitive line 97
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondPrimitive_coupling line 105
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondPrimitive_zero line 123
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondPrimitive_collars line 133
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondPath_isInvertible line 158
  11. def OAI.PackingSufficiencySupport.Hamiltonian.complexUnitDirection line 183
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexUnitDirection_coe line 190
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexUnitDirection_smoothAt line 195
  14. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexMap line 219
  15. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexInverse line 221
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexMap_smooth line 223
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexInverse_smoothAt line 235
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexMap_norm line 241
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexMap_ne_zero line 246
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplex_left_inv line 250
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplex_right_inv line 260
  22. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderComplexDiffeomorph line 266
  23. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart line 290
  24. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart_source line 293
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart_target line 297
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart_apply line 300
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart_symm_apply line 303
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart_smooth line 306
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realAnnulusChart_symm_smooth line 322
  30. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusDiffeomorph line 329
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusDiffeomorph_source line 335
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusDiffeomorph_target line 339
  33. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitCircle_subset_diffeomorph line 342
  34. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusPoint line 347
  35. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusPoint_zero line 351
  36. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusPoint_mem line 354
  37. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusDomain line 365
  38. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusDomain_isOpen line 368
  39. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitCircle_subset_transverseDomain line 382
  40. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusPoint_contDiffAt line 401
  41. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCoordinate line 415
  42. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCoordinate_apply line 419
  43. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCoordinate_point line 422
  44. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCoordinate_mul line 426
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCoordinate_ne_zero line 433
  46. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.inverse_transverseCoordinate line 440
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.plus_transverseCoordinate line 445
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.minus_transverseCoordinate line 450
  49. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseBranch line 455
  50. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusPoint_positive line 458
  51. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusPoint_coordinate line 464
  52. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusInverse line 482
  53. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusInverse_val line 486
  54. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseBranch_isOpen line 490
  55. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseAnnulusChart line 502
  56. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart line 531
  57. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart_source line 534
  58. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart_target line 538
  59. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart_apply line 541
  60. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart_symm_apply line 544
  61. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart_smooth line 547
  62. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.realTransverseChart_symm_smooth line 563
  63. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseDiffeomorph line 569
  64. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseDiffeomorph_source line 575
  65. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseDiffeomorph_target line 579
  66. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitCircle_subset_transverseDiffeomorph line 582