OAI/Geometry/BallPacking/Necessity/FrozenResponse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineCompose line 49
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderAffineCompose_value line 68
  3. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffCompact line 93
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCompact_value line 101
  5. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffFrozen line 111
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffFrozen_value line 117
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffFrozen_contDiff line 127
  8. def OAI.HigherDimensionalBallPacking.Rigidity.frozenResponse line 137
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenResponse_contDiffAt line 141
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenResponse_comp_contDiffAt line 155
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.frozenResponse_eq line 164
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffFrozen_eq line 175
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffFrozen_invertible line 212
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_curl_value line 224
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_curl_reconstruct line 234
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffFrozen_equation line 248
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1_frozen_response line 259