OAI/Geometry/BallPacking/Necessity/HolderCompactness.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.sectionApply line 36
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.sectionApply_norm line 43
  3. def OAI.HigherDimensionalBallPacking.Rigidity.sectionCLM line 51
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.sectionCLM_apply line 58
  5. def OAI.HigherDimensionalBallPacking.Rigidity.sectionOperatorCLM line 61
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.sectionOperatorCLM_apply line 71
  7. def OAI.HigherDimensionalBallPacking.Rigidity.superposeBCF line 76
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.superposeBCF_apply line 80
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.superposeBCF_uniformContinuous line 84
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.superposeBCF_hasFDerivAt line 103
  11. def OAI.HigherDimensionalBallPacking.Rigidity.compactCoefficient line 130
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactCoefficient_apply line 135
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactSuperpose_contDiff_nat line 138
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactSuperpose_contDiff line 160
  15. def OAI.HigherDimensionalBallPacking.Rigidity.adaptedJSection line 169
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.adaptedJSection_apply line 176
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.adaptedJSection_contDiff line 183
  18. def OAI.HigherDimensionalBallPacking.Rigidity.jetSectionEval line 192
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.jetSectionEval_apply line 195
  20. def OAI.HigherDimensionalBallPacking.Rigidity.bcfCRJet line 200
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.bcfCRJet_apply line 206
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.bcfCRJet_contDiff line 213
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.bcfCRJet_fderiv line 226
  24. def OAI.HigherDimensionalBallPacking.Rigidity.pairLeft line 278
  25. def OAI.HigherDimensionalBallPacking.Rigidity.pairRight line 283
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.pairLeft_apply line 288
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.pairRight_apply line 289
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.pairLeft_norm line 291
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.pairRight_norm line 293
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderValue_norm line 296
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderDifference_norm line 298
  32. def OAI.HigherDimensionalBallPacking.Rigidity.holderApply line 301
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderApply_value line 319
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderApply_norm line 323
  35. def OAI.HigherDimensionalBallPacking.Rigidity.holderCLM line 337
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCLM_apply line 353
  37. def OAI.HigherDimensionalBallPacking.Rigidity.holderOperatorLinear line 357
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderCLM_norm_bound line 377
  39. def OAI.HigherDimensionalBallPacking.Rigidity.holderOperatorCLM line 381
  40. lemma OAI.HigherDimensionalBallPacking.Rigidity.holder_norm_le_of_estimate line 393
  41. lemma OAI.HigherDimensionalBallPacking.Rigidity.holder_third_interpolation line 410
  42. lemma OAI.HigherDimensionalBallPacking.Rigidity.holder_third_small_sup line 430
  43. def OAI.HigherDimensionalBallPacking.Rigidity.holderLipschitzSet line 460
  44. def OAI.HigherDimensionalBallPacking.Rigidity.holderDiskRestrict line 464
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderDiskRestrict_apply line 469
  46. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderDiskRestrict_uniformInducing line 472
  47. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderLipschitzSet_totallyBounded line 501
  48. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderLipschitzSet_isCompact_closure line 528