OAI/Geometry/BallPacking/Forms/HorizontalCoupling.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_pullback line 23
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_isInvertible_coordinates line 39
  4. structure OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily line 67
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily.zero line 74
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily.add line 85
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily.smul line 98
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily.sum line 112
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily.const_slice line 123
  10. def OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior line 143
  11. def OAI.PackingSufficiencySupport.Hamiltonian.pathTimePrimitive line 147
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior_apply line 150
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior_smooth line 153
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathTimePrimitive_smooth line 162
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.fderiv_evaluation_const line 166
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior_fderiv line 173
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathTimePrimitive_fderiv line 188
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exact_path_time_equation line 196
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.exact_path_closed line 208
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior_smoothAt line 223
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathTimePrimitive_smoothAt line 232
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior_fderivAt line 236
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathTimePrimitive_fderivAt line 251
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.exact_path_time_equationAt line 259
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.exact_path_closedAt line 271
  26. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldTimePrimitive line 293
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_reconstruct_target line 296
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTimePrimitive_chart line 305
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.pathSpatialExterior_eq_slice line 339
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_path_chart line 352
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_path_smooth line 362
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTimePrimitive_smooth line 370
  33. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldWedge line 388
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldWedge_apply line 391
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldWedge_skew line 394
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_wedge line 399
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldWedge_smooth line 406
  38. def OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalarDifferential line 428
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalarDifferential_chart line 431
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalar_chart_smooth line 443
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalarDifferential_smooth line 449
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalarDifferential_closed line 462
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalarDifferential_support line 489
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_sub line 511
  45. def OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm line 517
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_inside line 521
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_outside line 526
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_off_support line 531
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_smooth line 538
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_exterior line 553
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_time line 569
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.glueManifoldOneForm_initial line 588