OAI/Geometry/BallPacking/Necessity/HolderCalculus.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.normalizedFrameCoefficient line 34
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedFrameCoefficient_smooth line 38
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedFrameCoefficient_compact line 59
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.linearizedCR_normalizedFrame line 69
  5. def OAI.HigherDimensionalBallPacking.Rigidity.framedMarkedVariation line 98
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRInverse_differentiable line 103
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedMarkedVariation_zero line 109
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.framedMarkedVariation_one line 114
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_marked_fredholm_linearization line 120
  10. abbrev OAI.HigherDimensionalBallPacking.Rigidity.UnitTime line 163
  11. def OAI.HigherDimensionalBallPacking.Rigidity.unitExtend line 165
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.unitExtend_coe line 169
  13. def OAI.HigherDimensionalBallPacking.Rigidity.unitMean line 172
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.unitMean_norm line 188
  15. def OAI.HigherDimensionalBallPacking.Rigidity.sectionMean line 193
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.sectionMean_apply line 203
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.sectionMean_norm line 207
  18. def OAI.HigherDimensionalBallPacking.Rigidity.sectionMeanCLM line 213
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.sectionMeanCLM_apply line 232
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactCoefficient_lipschitz line 252
  21. def OAI.HigherDimensionalBallPacking.Rigidity.holderPost line 259
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPost_apply line 271
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.segmentSection_bound line 277
  24. def OAI.HigherDimensionalBallPacking.Rigidity.segmentSection line 288
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.segmentSection_apply line 313
  26. def OAI.HigherDimensionalBallPacking.Rigidity.differencePull line 316
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.differencePull_apply line 319
  28. def OAI.HigherDimensionalBallPacking.Rigidity.holderPostDifference line 324
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderSegment_contDiff line 330
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCoefficient_contDiff line 335
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCoefficientOperator_contDiff line 343
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPostIntegrand_contDiff line 351
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPostDifference_contDiff line 359
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPostDifference_integral line 365
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPostDifference_relation line 379
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPost_coe line 406
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPost_ambient_contDiff line 422
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.holder_hasFDerivAt_of_ambient line 436
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPost_hasFDerivAt line 477
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPost_contDiff_nat line 494
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderPost_contDiff line 508