OAI/Geometry/BallPacking/Layers/ConstructedSurfaceLayers.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_final_surface_layer_packing line 14
  2. structure OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy line 99
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.map_smooth line 115
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.map_inverse_smooth line 118
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.compact_displacement line 121
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_pointwise_fderiv_isInvertible line 134
  7. def OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianBaseShear line 162
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianBaseShear_smooth line 173
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianBaseShear_inverse_smooth line 178
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianBaseShear_fderiv line 183
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianBaseShear_fderiv_isInvertible line 200
  12. def OAI.PackingSufficiencySupport.Hamiltonian.baseShearPrimitiveCoefficient line 207
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShearPrimitiveCoefficient_smooth line 210
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShearPrimitiveCoefficient_vertical line 216
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.hamiltonianBaseShear_suspension line 230
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_pullback_horizontal line 261
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_coupling_pullback line 272
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_coupling_isInvertible line 314
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_pullback_horizontal_general line 328
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_coupling_pullback_general line 339
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_weighted_isInvertible line 387
  22. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPrimitive line 415
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPrimitive_smooth line 423
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPrimitive_zero line 445
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPrimitive_lower line 454
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPrimitive_upper line 463
  27. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceInterpolatedLayer line 474
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceInterpolatedLayer_endpoints line 479