OAI/Geometry/BallPacking/Necessity/NonlinearCR.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.scalarSectionCLM line 43
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.scalarSectionCLM_apply line 54
  3. def OAI.HigherDimensionalBallPacking.Rigidity.pairDistance line 57
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.pairDistance_apply line 61
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.pairDistance_pos line 64
  6. def OAI.HigherDimensionalBallPacking.Rigidity.holderNearWeight line 66
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderNearWeight_apply line 75
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.divided_rpow_le_one line 78
  9. def OAI.HigherDimensionalBallPacking.Rigidity.holderFarWeight line 87
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderFarWeight_apply line 97
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderFarWeight_relation line 100
  12. def OAI.HigherDimensionalBallPacking.Rigidity.holderBaseDifference line 109
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderBaseDifference_apply line 136
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderBaseDifference_relation line 141
  15. def OAI.HigherDimensionalBallPacking.Rigidity.baseSegment line 149
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.baseSegment_apply line 152
  17. def OAI.HigherDimensionalBallPacking.Rigidity.profileWeightedDifference line 157
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.profileWeightedDifference_relation line 162
  19. def OAI.HigherDimensionalBallPacking.Rigidity.profilePostDifference line 175
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.segment_fderiv_integral line 187
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.profilePostDifference_integral line 201
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.profilePostDifference_relation line 226
  23. def OAI.HigherDimensionalBallPacking.Rigidity.holderProfilePost line 250
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderProfilePost_apply line 258
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.profileWeightedDifference_contDiff line 279
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.profileCoefficient_contDiff line 286
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.profileCoefficientOperator_contDiff line 295
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.profilePostNear_contDiff line 305
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.profileValue_contDiff line 318
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.profilePostDifference_contDiff line 325
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderProfilePost_ambient_contDiff line 334
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderProfilePost_hasFDerivAt line 342
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderProfilePost_contDiff_nat line 360
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderProfilePost_contDiff line 379
  35. def OAI.HigherDimensionalBallPacking.Rigidity.holderConst line 402
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderConst_apply line 405
  37. def OAI.HigherDimensionalBallPacking.Rigidity.holderLinearPost line 408
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderLinearPost_apply line 411
  39. def OAI.HigherDimensionalBallPacking.Rigidity.holderJSection line 416
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderJSection_apply line 423
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderJSection_contDiff line 433
  42. def OAI.HigherDimensionalBallPacking.Rigidity.holderJetEval line 441
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderJetEval_apply line 446
  44. def OAI.HigherDimensionalBallPacking.Rigidity.holderCRJet line 450
  45. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCRJet_apply line 458
  46. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCRJet_contDiff line 469
  47. def OAI.HigherDimensionalBallPacking.Rigidity.realAffineProfile line 482
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.realAffineProfile_apply line 486
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.realAffineProfile_lipschitz line 490
  50. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineJet line 501
  51. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineJet_contDiff line 505
  52. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineCurve line 510
  53. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineCurve_hasFDerivAt line 513
  54. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineCurve_fderiv line 518
  55. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCR line 523
  56. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCR_contDiff line 530
  57. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCR_apply line 539