OAI/Geometry/BallPacking/Annuli/LayerCoordinates.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.stripChart_fderiv_at line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerChart_pullback_at line 24
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerChart_inverse_local line 39
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.inverse_layer_product_pullback_local line 98
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_ball_in_layer_local line 120
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.finite_layer_packing_local line 189
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiffAt_parameter_segment_integral line 253
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiffOn_parameter_segment_integral line 281
  9. def OAI.PackingSufficiencySupport.Hamiltonian.layerAreaIntegral line 301
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerAreaIntegral_smooth line 304
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerAreaIntegral_hasDerivAt line 313
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.layerAreaIntegral_pos line 325
  13. def OAI.PackingSufficiencySupport.Hamiltonian.areaLayerCoordinate line 341
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaLayerCoordinate_data line 345
  15. def OAI.PackingSufficiencySupport.Hamiltonian.twoCovectorForm line 385
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.twoCovectorForm_apply line 391
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.twoCovectorForm_skew line 397
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.twoCovectorForm_isInvertible line 404
  19. def OAI.PackingSufficiencySupport.Hamiltonian.horizontalOneForm line 448
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalOneForm_apply line 453
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalOneForm_smooth line 457
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalOneForm_fderiv line 462
  23. def OAI.PackingSufficiencySupport.Hamiltonian.horizontalCoupling line 472
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalCoupling_eq line 477