OAI/Geometry/BallPacking/Kahler/PhaseArea.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.Hamiltonian.PlanePhase line 15
  2. def OAI.PackingSufficiencySupport.Hamiltonian.phaseArea line 17
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_apply line 20
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_skew line 24
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_single_right line 32
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_single_left line 41
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_injective line 50
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.phase_decomposition line 59
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_surjective line 69
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_isInvertible line 78
  11. def OAI.PackingSufficiencySupport.Hamiltonian.phaseDot line 87
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDot_apply line 95
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDot_symm line 99
  14. def OAI.PackingSufficiencySupport.Hamiltonian.phaseSq line 105
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_nonneg line 107
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_smul line 113
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_smooth line 118
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_hasFDerivAt line 121
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_fderiv line 132
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_self line 137
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverse_chart_isEmbedding line 148
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverse_chart_pullback line 166
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverse_chart_composition_pullback line 193
  24. def OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap line 216
  25. def OAI.PackingSufficiencySupport.Hamiltonian.fsAffineMap line 219
  26. def OAI.PackingSufficiencySupport.Hamiltonian.phaseOpenBall line 222
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseOpenBall_open line 224
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.fs_den_pos line 227
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_smooth line 230
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsAffineMap_smoothOn line 237
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_sq line 248
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_gap line 254
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_mem line 260
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsAffineMap_fsBallMap line 267
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsAffineMap_sq line 275
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_fsAffineMap line 280
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_image line 295
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_injective line 303
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsAffineMap_isEmbedding line 306
  40. def OAI.PackingSufficiencySupport.Hamiltonian.fsBallDifferential line 313
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallDifferential_apply line 317
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_hasFDerivAt line 325
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_fderiv line 348
  44. def OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm line 353
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_apply line 357
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_pullback line 362
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsAffineMap_pullback line 375
  48. def OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive line 384
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive_smooth line 387
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive_fderiv line 394
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSPrimitive_exterior line 416
  52. def OAI.PackingSufficiencySupport.Hamiltonian.phaseJ line 424
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseJ_apply line 430
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseJ_sq line 434
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDot_J_right line 437
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDot_J_left line 444
  57. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_J_right line 448
  58. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_J_left line 455
  59. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseDot_J_J line 459
  60. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_eq_zero_iff line 463
  61. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseSq_pos line 478
  62. theorem OAI.PackingSufficiencySupport.Hamiltonian.phase_complex_cauchy line 481
  63. def OAI.PackingSufficiencySupport.Hamiltonian.horizontalSystem line 505
  64. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalSystem_apply line 511
  65. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalSystem_injective line 515
  66. theorem OAI.PackingSufficiencySupport.Hamiltonian.finrank_continuous_dual line 535
  67. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalSystem_isInvertible line 539
  68. def OAI.PackingSufficiencySupport.Hamiltonian.symplecticHorizontalLift line 551
  69. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticHorizontalLift_projects line 556
  70. theorem OAI.PackingSufficiencySupport.Hamiltonian.symplecticHorizontalLift_orthogonal line 562
  71. theorem OAI.PackingSufficiencySupport.Hamiltonian.bilinear_injective_of_taming line 576
  72. theorem OAI.PackingSufficiencySupport.Hamiltonian.bilinear_isInvertible_of_taming line 589
  73. theorem OAI.PackingSufficiencySupport.Hamiltonian.convex_form_taming line 599
  74. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_pullback_isInvertible line 614
  75. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_eq_exterior line 628
  76. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_smooth line 634
  77. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_closed line 638
  78. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_skew line 644
  79. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_J line 649
  80. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_positive line 654
  81. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineFSForm_isInvertible line 671
  82. def OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhase line 682
  83. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhase_none line 689
  84. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhase_some line 691
  85. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhase_injective line 694
  86. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affinePhase_I line 705
  87. def OAI.PackingSufficiencySupport.DiagonalQuadrics.realPhaseDerivative line 710
  88. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realPhaseDerivative_one line 714
  89. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realPhaseDerivative_I line 717
  90. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineFSForm_holomorphic_positive line 725