OAI/Geometry/BallPacking/Normal/QuadricMovingCone.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.ConeModel line 19
  2. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.ConeSpace line 20
  3. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.ConeTarget line 21
  4. def OAI.PackingSufficiencySupport.DiagonalQuadrics.movingConeCoordinates line 23
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.movingConeCoordinates_smooth line 26
  6. def OAI.PackingSufficiencySupport.DiagonalQuadrics.centralConeCoordinates line 39
  7. def OAI.PackingSufficiencySupport.DiagonalQuadrics.centralConePrimitive line 42
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.movingConeCoordinates_zero line 46
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.movingConeCoordinates_nonzero line 53
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_normal_exact_family line 65
  11. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalModel line 97
  12. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalSpace line 98
  13. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCouplingPrimitive line 100
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCouplingPrimitive_smooth line 103
  15. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCouplingPrimitive_exterior line 112
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCoupling_invertible line 130
  17. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPhaseCoordinates line 149
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPhaseCoordinates_smooth line 152
  19. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPhaseCoordinates_derivative line 156
  20. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.centralConeCoordinates_smooth line 172
  21. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.cone_radial_primitive line 177
  22. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.LargeNormalModel line 220
  23. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.LargeNormalSpace line 221
  24. def OAI.PackingSufficiencySupport.DiagonalQuadrics.largeCouplingPrimitive line 223
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeHorizontal_lift_smooth line 226
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeCouplingPrimitive_smooth line 233
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeCouplingPrimitive_exterior line 241
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.phaseMoments_sum line 248
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalCouplingPrimitive_apply line 252
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeCouplingPrimitive_apply line 260
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.firstTailMap_primitive line 275
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeCouplingPrimitive_invertible line 304
  33. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_compact_first_tail_bridge line 329
  34. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_compact_radial_bridge line 405
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.movingPrimitivePullback_comp_eq line 476
  36. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_normal_primitive_family line 503
  37. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_radial_primitive_family line 533
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineBaseMap_isEmbedding_on line 590
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineMoving_smooth line 604
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineBaseMap_primitive_eq line 613
  41. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_large_normal_transfer line 636