OAI/Geometry/BallPacking/Forms/CubicFubiniStudy.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.CubicModel.planeAffine line 14
  2. theorem OAI.PackingSufficiencySupport.CubicModel.planeAffine_injective line 18
  3. def OAI.PackingSufficiencySupport.CubicModel.projectiveInclusion line 23
  4. def OAI.PackingSufficiencySupport.CubicModel.phaseInclusion line 24
  5. theorem OAI.PackingSufficiencySupport.CubicModel.phaseInclusion_smooth line 27
  6. def OAI.PackingSufficiencySupport.CubicModel.curveFSPrimitive line 34
  7. def OAI.PackingSufficiencySupport.CubicModel.curveFSForm line 36
  8. theorem OAI.PackingSufficiencySupport.CubicModel.curveFSPrimitive_smooth line 39
  9. theorem OAI.PackingSufficiencySupport.CubicModel.curveFSForm_smooth line 48
  10. theorem OAI.PackingSufficiencySupport.CubicModel.curveFSPrimitive_exterior line 60
  11. theorem OAI.PackingSufficiencySupport.CubicModel.curveFSForm_skew line 75
  12. def OAI.PackingSufficiencySupport.CubicModel.cubicChart line 78
  13. theorem OAI.PackingSufficiencySupport.CubicModel.cubicChart_smooth line 81
  14. theorem OAI.PackingSufficiencySupport.CubicModel.cubicChart_derivative_one_ne line 86
  15. theorem OAI.PackingSufficiencySupport.CubicModel.phase_chart_function line 116
  16. theorem OAI.PackingSufficiencySupport.CubicModel.phase_chart_derivative line 125
  17. theorem OAI.PackingSufficiencySupport.CubicModel.curveFSForm_positive line 138
  18. def OAI.PackingSufficiencySupport.CubicModel.weightedProjection line 151
  19. def OAI.PackingSufficiencySupport.CubicModel.weightedHomogeneous line 154
  20. theorem OAI.PackingSufficiencySupport.CubicModel.weightedProjection_contDiff line 157
  21. theorem OAI.PackingSufficiencySupport.CubicModel.weightedHomogeneous_homogeneous line 166
  22. theorem OAI.PackingSufficiencySupport.CubicModel.weightedProjection_fderiv_fst line 191
  23. theorem OAI.PackingSufficiencySupport.CubicModel.weightedProjection_fderiv_snd line 204
  24. theorem OAI.PackingSufficiencySupport.CubicModel.weightedProjection_fderiv_kernel line 217
  25. def OAI.PackingSufficiencySupport.CubicModel.weightedInclusion line 229
  26. theorem OAI.PackingSufficiencySupport.CubicModel.weightedInclusion_smooth line 232
  27. def OAI.PackingSufficiencySupport.CubicModel.weightedChart line 236
  28. theorem OAI.PackingSufficiencySupport.CubicModel.weightedChart_smooth line 239
  29. theorem OAI.PackingSufficiencySupport.CubicModel.weightedChart_derivative_one_ne line 244
  30. def OAI.PackingSufficiencySupport.CubicModel.weightedPhaseInclusion line 263
  31. theorem OAI.PackingSufficiencySupport.CubicModel.weightedPhaseInclusion_smooth line 266
  32. def OAI.PackingSufficiencySupport.CubicModel.weightedFSPrimitive line 273
  33. def OAI.PackingSufficiencySupport.CubicModel.weightedFSForm line 275
  34. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSPrimitive_smooth line 278
  35. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSForm_smooth line 287
  36. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSPrimitive_exterior line 299
  37. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSForm_skew line 314
  38. theorem OAI.PackingSufficiencySupport.CubicModel.weighted_phase_chart_function line 317
  39. theorem OAI.PackingSufficiencySupport.CubicModel.weighted_phase_chart_derivative line 326
  40. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSForm_positive line 339
  41. def OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPoint line 363
  42. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPoint_contDiffAt line 365
  43. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityRegularPoint_fderiv line 369
  44. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.infinityPoint_fderiv line 377
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.realPhaseDerivative_fderiv line 394
  46. def OAI.PackingSufficiencySupport.DiagonalQuadrics.complexArea line 405
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complexArea_apply line 407
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complexArea_sub line 411
  49. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complexArea_mul line 414
  50. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complexArea_self_mul line 423
  51. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complex_div_im line 428
  52. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.complexArea_div_derivative line 432
  53. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.phaseSq_affinePhase line 442
  54. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.phaseArea_affinePhase line 447
  55. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineFSPrimitive_complex line 451
  56. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.affineFSPrimitive_projective_swap line 459
  57. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldMapDifferential_comp line 495
  58. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackOneForm_comp line 502