OAI/Geometry/BallPacking/Annuli/AnnularCurvaturePrimitive.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.annularRadialIntegral line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularRadialIntegral_smooth line 17
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularRadialIntegral_periodic line 30
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularRadialIntegral_hasDerivAt line 42
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCovector_exterior_at line 54
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.annular_curvature_primitive line 75
  7. def OAI.PackingSufficiencySupport.Hamiltonian.handleCutPoint line 106
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleCutPoint_ne_one line 108
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortCircleArgument_cutPoint line 116
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleCutPoint_not_band line 126
  11. def OAI.PackingSufficiencySupport.Hamiltonian.compactHandleBand line 132
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactHandleBand_isCompact line 135
  13. def OAI.PackingSufficiencySupport.Hamiltonian.handlePuncture line 138
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePuncture_not_compactBand line 140
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_torus_handle_away_from_puncture line 148
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.torus_fst_smooth line 185
  17. def OAI.PackingSufficiencySupport.Hamiltonian.torusFirstForm line 191
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusFirstForm_apply line 194
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusFirstForm_smooth line 201
  20. def OAI.PackingSufficiencySupport.Hamiltonian.torusTurns line 216
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatPlane_fst_smooth line 218
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatPlane_snd_smooth line 221
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusTurns_smooth line 224
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusTurns_derivative line 230
  25. def OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity line 255
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_smooth line 258
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_turns line 264
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_support line 295
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_tsupport line 320
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_normalized line 325
  31. def OAI.PackingSufficiencySupport.Hamiltonian.angularUnitVector line 346
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularUnitVector_value line 349
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleAngular_injective line 353
  34. def OAI.PackingSufficiencySupport.Hamiltonian.torusAreaForm line 370
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAreaForm_apply line 373
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAreaForm_smooth line 378
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAreaForm_skew line 382
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAreaForm_isInvertible line 386
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_eq_multiple line 408
  40. def OAI.PackingSufficiencySupport.Hamiltonian.annularCylinderScalar line 427
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCylinderScalar_smoothAt line 430
  42. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderCurvaturePrimitive line 455
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCurvaturePrimitive_smoothAt line 459
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCurvaturePrimitive_cover line 471
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCurvaturePrimitive_exterior_cover line 485
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_derivative_right_inverse line 521
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover_derivative_right_inverse line 525
  48. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderAreaForm line 531
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderAreaForm_apply line 534
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCurvaturePrimitive_exterior_covered line 541
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCurvaturePrimitive_exterior line 564