OAI/Geometry/BallPacking/Rigidity/CompatibleStructures.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HigherDimensionalBallPacking.Phase line 8

    Also declared: ComparatorChallenges/BallPacking.lean:8 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:8 (same declaration text).

  2. def OAI.HigherDimensionalBallPacking.capacity line 10

    Also declared: ComparatorChallenges/BallPacking.lean:10 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:10 (same declaration text).

  3. def OAI.HigherDimensionalBallPacking.closedBall line 13

    Also declared: ComparatorChallenges/BallPacking.lean:13 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:13 (same declaration text).

  4. def OAI.HigherDimensionalBallPacking.openBall line 15

    Also declared: ComparatorChallenges/BallPacking.lean:15 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:15 (same declaration text).

  5. def OAI.HigherDimensionalBallPacking.standardForm line 17

    Also declared: ComparatorChallenges/BallPacking.lean:17 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:17 (same declaration text).

  6. def OAI.HigherDimensionalBallPacking.SymplecticOn line 20

    Also declared: ComparatorChallenges/BallPacking.lean:20 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:21 (same declaration text).

  7. def OAI.HigherDimensionalBallPacking.HasPacking line 26

    Also declared: ComparatorChallenges/BallPacking.lean:26 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:28 (same declaration text).

  8. def OAI.HigherDimensionalBallPacking.PackingInequalities line 33

    Also declared: ComparatorChallenges/BallPacking.lean:33 (same declaration text), ComparatorChallenges/BallPackingNecessity.lean:35 (same declaration text).

  9. abbrev OAI.HigherDimensionalBallPacking.Rigidity.End line 42
  10. def OAI.HigherDimensionalBallPacking.Rigidity.standardJ line 44
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardJ_apply line 47
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardJ_sq line 50
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_J_J line 55
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_J_self line 63
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_J_pos line 70
  16. def OAI.HigherDimensionalBallPacking.Rigidity.Compatible line 81
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.compatible_standardJ line 86
  18. def OAI.HigherDimensionalBallPacking.Rigidity.conjugateJ line 89
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.conjugateJ_apply line 92
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.compatible_conjugateJ line 95
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplectic_linear_injective line 115
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplectic_linear_invertible line 127
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_fderiv_invertible line 134
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_injOn line 139
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_open_image line 144
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_inverse_smooth line 156
  27. def OAI.HigherDimensionalBallPacking.Rigidity.imageJ line 179
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.imageJ_at_image line 183
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.imageJ_compatible line 190
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.imageJ_smooth line 205
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.imageJ_intertwines line 219
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_inverse_fderiv line 228
  33. def OAI.HigherDimensionalBallPacking.Rigidity.PseudoHolomorphicAt line 254
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.complex_differentiable_of_CR line 258
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverse_chart_holomorphic line 282
  36. def OAI.HigherDimensionalBallPacking.Rigidity.stdDot line 311
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_apply line 319
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_symm line 323
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_J_right line 329
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_pos line 333
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_nonneg line 337
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_skew line 343
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_neg_right line 351
  44. theorem OAI.HigherDimensionalBallPacking.Rigidity.compatible_metric_symm line 360
  45. theorem OAI.HigherDimensionalBallPacking.Rigidity.compatible_of_sq_symmetric_positive line 367
  46. def OAI.HigherDimensionalBallPacking.Rigidity.relativeOperator line 375
  47. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeOperator_apply line 377
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardJ_relativeOperator line 380
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeOperator_J_relativeOperator line 383
  50. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_relativeOperator line 389
  51. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeOperator_selfadjoint line 393
  52. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeOperator_positive line 399
  53. def OAI.HigherDimensionalBallPacking.Rigidity.cayleyP line 404
  54. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyP_apply line 407
  55. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyP_invertible line 410
  56. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyP_commute line 430
  57. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyP_J_identity line 435
  58. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyP_stdDot_identity line 442
  59. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyP_stdDot_positive line 451
  60. def OAI.HigherDimensionalBallPacking.Rigidity.cayleyOperator line 468
  61. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyOperator_on_denominator line 471
  62. theorem OAI.HigherDimensionalBallPacking.Rigidity.denominator_cayleyOperator line 479
  63. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyOperator_selfadjoint line 487
  64. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyOperator_positive line 499
  65. theorem OAI.HigherDimensionalBallPacking.Rigidity.cayleyOperator_J_identity line 509
  66. def OAI.HigherDimensionalBallPacking.Rigidity.interpolateJ line 520
  67. theorem OAI.HigherDimensionalBallPacking.Rigidity.compatible_interpolateJ line 523
  68. theorem OAI.HigherDimensionalBallPacking.Rigidity.interpolateJ_zero line 543
  69. theorem OAI.HigherDimensionalBallPacking.Rigidity.interpolateJ_one line 553
  70. theorem OAI.HigherDimensionalBallPacking.Rigidity.contDiffAt_interpolateJ line 565