OAI/Geometry/BallPacking/Surfaces/QuadricAnnulusDomain.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.plus_contDiffAt line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.minus_contDiffAt line 18
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.baseSquare_contDiffAt line 21
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusDomain_isOpen line 24
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitCircle_subset_domain line 40
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint_contDiffAt line 59
  7. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusCoordinate line 83
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusCoordinate_apply line 87
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusCoordinate_point line 89
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusCoordinate_mul line 92
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusCoordinate_ne_zero line 100
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.inverse_coordinate line 107
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.plus_coordinate line 112
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.minus_coordinate line 117
  15. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.baseSquare_coordinate line 122
  16. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.Surface line 129
  17. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusBranch line 131
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint_positive line 134
  19. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusPoint_coordinate line 144
  20. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusBasepoint line 172
  21. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusInverse line 174
  22. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusInverse_val line 178
  23. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusBranch_isOpen line 182
  24. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusChart line 196
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusChart_apply line 225
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusChart_source line 226
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusChart_target line 227
  28. abbrev OAI.PackingSufficiencySupport.CubicModel.PlaneBase line 236
  29. abbrev OAI.PackingSufficiencySupport.CubicModel.BaseCurve line 237
  30. def OAI.PackingSufficiencySupport.CubicModel.polynomial line 239
  31. def OAI.PackingSufficiencySupport.CubicModel.homogeneous line 240
  32. def OAI.PackingSufficiencySupport.CubicModel.projection line 241
  33. def OAI.PackingSufficiencySupport.CubicModel.inclusion line 242
  34. theorem OAI.PackingSufficiencySupport.CubicModel.polynomial_contDiff line 244
  35. theorem OAI.PackingSufficiencySupport.CubicModel.projection_contDiff line 248
  36. theorem OAI.PackingSufficiencySupport.CubicModel.source_equation_zero line 252
  37. theorem OAI.PackingSufficiencySupport.CubicModel.source_equation_one line 254
  38. theorem OAI.PackingSufficiencySupport.CubicModel.inclusion_polynomial line 257
  39. theorem OAI.PackingSufficiencySupport.CubicModel.inclusion_fst_ne_zero line 263
  40. theorem OAI.PackingSufficiencySupport.CubicModel.inclusion_snd_ne_zero line 271
  41. def OAI.PackingSufficiencySupport.CubicModel.recovery line 279
  42. theorem OAI.PackingSufficiencySupport.CubicModel.recovery_inclusion line 283
  43. theorem OAI.PackingSufficiencySupport.CubicModel.inclusion_contMDiff line 298
  44. theorem OAI.PackingSufficiencySupport.CubicModel.recovery_contDiffOn line 301
  45. theorem OAI.PackingSufficiencySupport.CubicModel.inclusion_isEmbedding line 314
  46. def OAI.PackingSufficiencySupport.CubicModel.gradV line 324
  47. def OAI.PackingSufficiencySupport.CubicModel.gradW line 325
  48. def OAI.PackingSufficiencySupport.CubicModel.jacobian line 326
  49. theorem OAI.PackingSufficiencySupport.CubicModel.polynomial_hasFDerivAt line 329
  50. theorem OAI.PackingSufficiencySupport.CubicModel.gradient_nonzero line 341
  51. theorem OAI.PackingSufficiencySupport.CubicModel.jacobian_surjective line 354
  52. theorem OAI.PackingSufficiencySupport.CubicModel.marked_points line 363
  53. theorem OAI.PackingSufficiencySupport.CubicModel.homogeneous_affine line 366