OAI/Geometry/BallPacking/Forms/QuadricInfinityPrimitive.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPhase line 15
  2. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPrimitive line 18
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPhase_contDiffAt line 21
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPrimitive_contDiffAt line 28
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPrimitive_apply line 34
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPhase_germ line 54
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveFSPrimitive_infinity line 64
  8. def OAI.PackingSufficiencySupport.Hamiltonian.complexCartesianLinear line 114
  9. def OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian line 122
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_apply line 125
  11. def OAI.PackingSufficiencySupport.Hamiltonian.complexPairing line 128
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPairing_re line 130
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPairing_im line 138
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_sq line 146
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPairing_self line 150
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_I line 154
  17. def OAI.PackingSufficiencySupport.Hamiltonian.complexDiagonal line 158
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexDiagonal_apply line 163
  19. def OAI.PackingSufficiencySupport.Hamiltonian.phaseDiagonal line 166
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDiagonal_cartesian line 170
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexDiagonal_pairing line 175
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDiagonal_dot line 185
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDiagonal_area line 192
  24. def OAI.PackingSufficiencySupport.Hamiltonian.phaseUnitDiagonal line 199
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseUnitDiagonal_apply line 226
  26. def OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift line 229
  27. def OAI.PackingSufficiencySupport.Hamiltonian.complexAffineQuotient line 233
  28. def OAI.PackingSufficiencySupport.Hamiltonian.affineSphereScale line 235
  29. def OAI.PackingSufficiencySupport.Hamiltonian.complexSphereLift line 237
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_none line 240
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_some line 242
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_smooth line 244
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_sq line 251
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineSphereScale_pos line 256
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineSphereScale_smooth line 259
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexSphereLift_smooth line 268
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexSphereLift_sq line 271
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexSphereLift_none_ne line 278
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineQuotient_smoothAt line 282
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineQuotient_smul line 291
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineQuotient_lift line 298
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineQuotient_sphereLift line 301
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_quotient line 308
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_complex_smul_sq line 315
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexSphereLift_quotient_unit line 319
  46. def OAI.PackingSufficiencySupport.Hamiltonian.parameterPullbackOneForm line 340
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_parameterPullbackOneForm line 346
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterPullbackOneForm_smooth line 373
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.add line 405
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.smul line 412
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.comp line 419
  52. def OAI.PackingSufficiencySupport.Hamiltonian.movingPrimitivePullback line 435
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.movingPrimitivePullback_smooth line 439
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.movingPrimitivePullback_exterior line 449
  55. def OAI.PackingSufficiencySupport.Hamiltonian.extendManifoldOneForm line 469
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendManifoldOneForm_inside line 474
  57. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendManifoldOneForm_outside line 480
  58. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendManifoldOneForm_smooth line 485
  59. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendManifoldOneForm_compact line 522
  60. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_congr_of_eventuallyEq line 531
  61. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendManifoldOneForm_exterior_inside line 549