OAI/Geometry/PolarProducts/MomentumBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolarStrips.position_mem_interior line 42
  2. theorem OAI.PolarStrips.norm_re_le line 51
  3. theorem OAI.PolarStrips.momentum_bound line 55
  4. theorem OAI.PolarStrips.exists_uniform_momentum_bound line 93
  5. theorem OAI.PolarStrips.exists_scaled_image line 109
  6. theorem OAI.LocalEmbedding.open_image line 160
  7. theorem OAI.LocalEmbedding.isOpenEmbedding line 174
  8. theorem OAI.SymmetricPolar.isOpen_capacityBall line 197
  9. def OAI.SymmetricPolar.diagScale line 200
  10. theorem OAI.SymmetricPolar.diagScale_apply line 204
  11. theorem OAI.SymmetricPolar.diagScale_injective line 206
  12. theorem OAI.SymmetricPolar.omega0_diagScale line 212
  13. theorem OAI.SymmetricPolar.omega0_nondegenerate line 217
  14. theorem OAI.SymmetricPolar.isInvertible_of_preserves_omega0 line 224
  15. theorem OAI.SymmetricPolar.hasSymplecticEmbedding_of_injOn line 238
  16. theorem OAI.SymmetricPolar.HasSymplecticEmbedding.mono_target line 246
  17. theorem OAI.SymmetricPolar.HasSymplecticEmbedding.injOn line 251
  18. theorem OAI.SymmetricPolar.mapsTo_scaled_ball line 256
  19. theorem OAI.SymmetricPolar.embedding_of_scaled_ball_map line 266