OAI/Geometry/BallPacking/Necessity/FrameFredholm.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderValue_bound line 45
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderDeriv_bound line 50
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderValue_lipschitz line 55
  4. def OAI.HigherDimensionalBallPacking.Rigidity.c1LowerOrderCLM line 62
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1LowerOrderCLM_value line 66
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1LowerOrder_image_lipschitz line 71
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1LowerOrderCLM_compact line 101
  8. def OAI.HigherDimensionalBallPacking.Rigidity.holderConstantCLM line 141
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderConstantCLM_value line 152
  10. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderEval line 155
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.c1HolderEval_apply line 158
  12. def OAI.HigherDimensionalBallPacking.Rigidity.markedLowerOrderAmbient line 163
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedLowerOrderAmbient_value line 172
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedLowerOrderAmbient_compact line 182
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.boundedLipschitz_holder_estimate line 214
  16. def OAI.HigherDimensionalBallPacking.Rigidity.holderOfLipschitz line 232
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderOfLipschitz_apply line 237
  18. def OAI.HigherDimensionalBallPacking.Rigidity.compactSmoothHolder line 241
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactSmoothHolder_apply line 246
  20. def OAI.HigherDimensionalBallPacking.Rigidity.smoothHolderField line 299
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothHolderField_value line 304
  22. def OAI.HigherDimensionalBallPacking.Rigidity.slopeCoefficient line 308
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.slopeCoefficient_apply line 312
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.slopeCoefficient_smooth line 316
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.slopeCoefficient_compact line 321
  26. def OAI.HigherDimensionalBallPacking.Rigidity.markedCRLower line 329
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRLower_value line 340
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRLower_compact line 349
  29. def OAI.HigherDimensionalBallPacking.Rigidity.markedCRLinear line 362
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRLinear_differential line 368
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.markedCRLinear_fredholm line 378
  32. def OAI.HigherDimensionalBallPacking.Rigidity.CompatibleWith line 391
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.CompatibleWith.form_left line 395
  34. def OAI.HigherDimensionalBallPacking.Rigidity.relativeTransition line 402
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeTransition_apply line 405
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeTransition_apply_B line 408
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeTransition_positive_identity line 413
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeTransition_positive line 424
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.relativeTransition_isInvertible line 437
  40. def OAI.HigherDimensionalBallPacking.Rigidity.crOperator line 451
  41. def OAI.HigherDimensionalBallPacking.Rigidity.crJet line 455
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.crJet_smooth line 458
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.crJet_fderiv line 465
  44. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactSupport_comp_proper line 490
  45. def OAI.HigherDimensionalBallPacking.Rigidity.crFrame line 499
  46. theorem OAI.HigherDimensionalBallPacking.Rigidity.crFrame_intertwines line 502
  47. theorem OAI.HigherDimensionalBallPacking.Rigidity.crFrame_smooth line 509
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.crFrame_invertible line 515
  49. def OAI.HigherDimensionalBallPacking.Rigidity.linearizedCR line 521
  50. theorem OAI.HigherDimensionalBallPacking.Rigidity.linearizedCR_jet line 525
  51. def OAI.HigherDimensionalBallPacking.Rigidity.frameLowerOrder line 533
  52. theorem OAI.HigherDimensionalBallPacking.Rigidity.linearizedCR_frame line 539
  53. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactSupport_fderiv_sub_const line 552
  54. theorem OAI.HigherDimensionalBallPacking.Rigidity.crFrame_compact_difference line 561
  55. theorem OAI.HigherDimensionalBallPacking.Rigidity.frameLowerOrder_compact line 574