OAI/Geometry/BallPacking/Normal/TailLineCoordinates.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.normalTail line 12
  2. def OAI.PackingSufficiencySupport.Hamiltonian.normalHead line 14
  3. def OAI.PackingSufficiencySupport.Hamiltonian.normalSplit line 16
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalSplit_liouville line 25
  5. def OAI.PackingSufficiencySupport.Hamiltonian.firstTailMap line 37
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstTailMap_smooth line 41
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstTailMap_derivative line 55
  8. def OAI.PackingSufficiencySupport.DiagonalQuadrics.regularLocus line 98
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.regularLocus_isOpen line 100
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.locus_subset_regularLocus line 103
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.regular_jacobian_surjective line 109
  12. def OAI.PackingSufficiencySupport.DiagonalQuadrics.realJacobian line 116
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.equations_real_hasFDerivAt line 119
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realJacobian_contDiff line 123
  15. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalLift line 130
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalLift_projects line 133
  17. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalLift_contDiffOn line 137
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_compact_normal_lift line 143
  19. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_normal_tube line 164
  20. def OAI.PackingSufficiencySupport.Hamiltonian.normalRadial line 222
  21. def OAI.PackingSufficiencySupport.Hamiltonian.normalRadialInverse line 225
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadial_smoothOn line 228
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadialInverse_smooth line 234
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadial_leftInverse line 241
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadial_rightInverse line 247
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadial_isEmbedding line 252
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseArea_radial_derivative line 263
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadial_sq line 274
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalRadial_area line 280
  30. def OAI.PackingSufficiencySupport.Hamiltonian.coneDenominator line 301
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.coneDenominator_pos line 304
  32. def OAI.PackingSufficiencySupport.Hamiltonian.conePrimitive line 307
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.conePrimitive_apply line 314
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.conePrimitive_smooth line 318
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.coneDenominator_normalRadial line 338
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.conePrimitive_radial_pullback line 347
  37. def OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese line 381
  38. def OAI.PackingSufficiencySupport.Hamiltonian.joinedVeroneseDerivative line 384
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_smooth line 391
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_hasFDerivAt line 398
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_sq line 409
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_pairing line 416
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_area line 424
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_real_derivative line 432
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.joinedVeronese_primitive line 442
  46. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalGraph line 463
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalGraph_smooth line 467
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPolynomial_eq_joined line 471
  49. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalConeCoordinates line 476
  50. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalConeCoordinates_smooth line 480
  51. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalGraph_derivative_fst line 485
  52. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalConeCoordinates_derivative line 494
  53. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalPolynomial_derivative_joined line 511
  54. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalAmbientPrimitive_eq_cone line 529