OAI/Geometry/BallPacking/Projective/AnnularChartHelpers.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_sub_at line 20
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterManifoldPullbackOneForm_inverse_apply line 38
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.IsPrimitiveFamily.intrinsic line 59
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_add_at line 74
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_smul_at line 89
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_model line 108
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_model line 115
  8. def OAI.PackingSufficiencySupport.Hamiltonian.linearLiouville line 123
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.linearLiouville_smooth line 127
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.linearLiouville_exterior line 132
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.flatProduct_snd_derivative line 144
  12. def OAI.PackingSufficiencySupport.Hamiltonian.productVerticalLiouville line 150
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.productVerticalLiouville_apply line 154
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.productVerticalLiouville_smooth line 160
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.productVerticalLiouville_exterior line 167
  16. def OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive line 180
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive_smooth line 184
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.productCouplingPrimitive_exterior line 189
  19. def OAI.PackingSufficiencySupport.Hamiltonian.standardLiouville line 205
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.standardLiouville_smooth line 208
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.standardLiouville_exterior line 211
  22. def OAI.PackingSufficiencySupport.Hamiltonian.verticalLiouville line 224
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.verticalLiouville_apply line 228
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.verticalLiouville_smooth line 234
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.verticalLiouville_exterior line 242
  26. def OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback line 262
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback_smooth line 265
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback_exterior line 270
  29. def OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive line 290
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_smoothAt line 293
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_fderiv line 298
  32. def OAI.PackingSufficiencySupport.Hamiltonian.hopfForm line 318
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_apply line 320
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_radial line 327
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_circle line 330
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_radial line 337
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_circle line 344
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_complex_diagonal line 352
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_semipositive line 360
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_complex_smul line 365
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_skew line 369
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_complex_line line 374
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPairing_complex_smul line 380
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_smul_dot line 388
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexCartesian_smul_area line 394
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_complex_scale line 400
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfForm_variable_gauge line 417
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_complex_line line 450
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_complex_scale line 457
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_variable_gauge line 467
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexAffineLift_derivative line 491
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive_hopf line 508
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive_hopf_pullback line 518