OAI/Geometry/BallPacking/Necessity/MarkedProfiles.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCR_fderiv line 40
  2. def OAI.HigherDimensionalBallPacking.Rigidity.holderConstCLM line 90
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderConstCLM_apply line 100
  4. def OAI.HigherDimensionalBallPacking.Rigidity.holderSourceCutoff line 105
  5. def OAI.HigherDimensionalBallPacking.Rigidity.holderSourceCutoffLinear line 109
  6. def OAI.HigherDimensionalBallPacking.Rigidity.holderCutoffAffine line 114
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCutoffAffine_apply line 120
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCutoffAffine_contDiff line 126
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineProfile_lower_bound line 152
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactCoefficient_zero_outside line 177
  11. def OAI.HigherDimensionalBallPacking.Rigidity.holderAffineFamily line 187
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderAffineFamily_apply line 194
  13. def OAI.HigherDimensionalBallPacking.Rigidity.localizedAffineFamily line 200
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizedAffineFamily_contDiff line 208
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizedAffineFamily_apply line 218
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizedAffineFamily_eq line 230
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderAffineFamily_contDiffAt line 265
  18. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCRFamily line 314
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderCRFamily_contDiffAt line 320
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderGraph_mem_of_hasFDerivAt line 359
  21. def OAI.HigherDimensionalBallPacking.Rigidity.compactSmoothC1Holder line 376
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactSmoothC1Holder_value line 382
  23. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderMultiply line 388
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderMultiply_value line 403
  25. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderConstantCLM line 409
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderConstantCLM_value line 416
  27. def OAI.HigherDimensionalBallPacking.Rigidity.markedFramedProfile line 434
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedFramedProfile_value line 452
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedFramedProfile_marks line 466