OAI/Geometry/BallPacking/Annuli/SurfaceSuspensionCoefficients.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceSuspensionCoefficient line 14
  2. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstCorrectionCoefficient line 18
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSuspensionCoefficient_smooth line 22
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstCorrectionCoefficient_smooth line 30
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSuspensionCoefficient_zero line 40
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstCorrectionCoefficient_zero line 44
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstCorrectionCoefficient_tails line 49
  8. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleFirstCorrection line 65
  9. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive line 74
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleFirstCorrection_off_band line 82
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_off_band line 101
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_zero line 113
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_smooth line 123
  14. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondCorrectionCoefficient line 166
  15. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondExtraCoefficient line 172
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondCorrectionCoefficient_smooth line 178
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondExtraCoefficient_smooth line 195
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondExtraCoefficient_zero line 205
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondExtraCoefficient_tails line 213
  20. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleSecondExtra line 240
  21. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive line 248
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_zero line 258
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleSecondExtra_off_band line 270
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_off_band line 291
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_smooth line 309
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_normal line 346
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_normal line 365
  28. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover line 394
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_smoothAt line 398
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_derivative line 405
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.dual_cover line 414
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.radial_cover line 427
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_inverse line 441
  34. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverA line 454
  35. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCoverB line 459
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularCover_form_rep line 464
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceFirstPrimitive_cover line 476
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.globalSurfaceSecondPrimitive_cover line 515