OAI/Geometry/BallPacking/Necessity/OrbitRegularity.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.diagonalShift line 48
  2. def OAI.HigherDimensionalBallPacking.Rigidity.holderShift line 53
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderShift_value line 67
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderShift_norm line 71
  5. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderShift line 76
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderShift_value line 84
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderShift_Deriv line 88
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderShift_norm line 91
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_shift_value_holder_bound line 95
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_shift_value_continuous line 126
  11. def OAI.HigherDimensionalBallPacking.Rigidity.holderTranspose line 151
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderTranspose_value line 156
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.holder_hasFDerivAt line 160
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.holder_shift_value_hasFDerivAt line 200
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbit_response_comp line 227
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbit_gain line 236
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_orbit_contDiff line 249
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_orbit_smooth_function line 281
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_orbit_regular line 297
  20. def OAI.HigherDimensionalBallPacking.Rigidity.affineSlope line 328
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineSlope_apply line 331
  22. def OAI.HigherDimensionalBallPacking.Rigidity.orbitCoefficient line 333
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitCoefficient_contDiff line 337
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitCoefficient_value line 350
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitCoefficient_C1 line 360
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineCoefficient_exterior line 367
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitCoefficient_support line 377
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_shift_decay line 392
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_shift_curl line 397
  30. def OAI.HigherDimensionalBallPacking.Rigidity.orbitResponse line 433
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitResponseDensity_contDiffAt line 438
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitResponse_contDiffAt line 447
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.orbitResponse_identity line 456
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_c1_regular line 475