OAI/Geometry/BallPacking/Necessity/MarkedInverse.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.segmentIntegrand_continuous line 36
  2. def OAI.HigherDimensionalBallPacking.Rigidity.linearSegmentIntegral line 40
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.linearSegmentIntegral_apply line 57
  4. abbrev OAI.HigherDimensionalBallPacking.Rigidity.C1HolderAmbient line 60
  5. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderGraph line 63
  6. instance OAI.HigherDimensionalBallPacking.Rigidity.c1HolderGraph_isClosed line 80
  7. abbrev OAI.HigherDimensionalBallPacking.Rigidity.C1HolderSpace line 94
  8. instance OAI.HigherDimensionalBallPacking.Rigidity.c1HolderSpace_complete line 97
  9. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderValue line 100
  10. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderDeriv line 103
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderValue_apply line 106
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderDeriv_apply line 108
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.linearSegmentIntegral_remainder line 111
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1Holder_hasFDerivAt line 123
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1Holder_fderiv line 149
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1Holder_contDiff line 153
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderValue_injective line 167
  18. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderMk line 180
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderMk_value line 206
  20. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderSubmodule line 220
  21. instance OAI.HigherDimensionalBallPacking.Rigidity.compactHolderSubmodule_isClosed line 226
  22. abbrev OAI.HigherDimensionalBallPacking.Rigidity.CompactHolderSpace line 238
  23. instance OAI.HigherDimensionalBallPacking.Rigidity.compactHolderSpace_complete line 241
  24. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue line 244
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue_apply line 247
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue_support line 250
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue_compactSupport line 258
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue_bound line 262
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderValue_holder line 266
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchy_exists line 283
  31. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchy line 299
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchy_value line 302
  33. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchyLM line 307
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchyLM_value line 329
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchy_continuous line 333
  36. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchyCLM line 359
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderCauchyCLM_value line 363
  38. def OAI.HigherDimensionalBallPacking.Rigidity.holderMap line 376
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderMap_value line 384
  40. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderMap line 389
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderMap_value line 397
  42. def OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverse line 408
  43. def OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverseValue line 412
  44. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverseValue_apply line 415
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverse_rightInverse line 419
  46. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverse_contDiff line 438
  47. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverse_tendsto_zero line 441
  48. def OAI.HigherDimensionalBallPacking.Rigidity.markedCRInverse line 453
  49. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRInverse_zero line 457
  50. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRInverse_one line 459
  51. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRInverse_rightInverse line 462