OAI/Geometry/BallPacking/Necessity/SchauderBounds.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactCRInverse_leftInverse line 36
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactCR_coercivity line 74
  3. def OAI.HigherDimensionalBallPacking.Rigidity.c1HolderDx line 100
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1HolderDx_value line 103
  5. def OAI.HigherDimensionalBallPacking.Rigidity.compactHolderApply line 109
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderApply_value line 118
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderApply_norm line 124
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactHolderApply_c1_norm line 129
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.absorb_half line 142
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.small_principal_coercivity line 148
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactSmoothHolder_interpolation line 191
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.c1Holder_fderiv_holder line 212
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.small_principal_smooth_estimate line 222
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.norm_fderiv_smul_bound line 272
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.norm_fderiv_apply_bound line 281
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smul_bounds line 291
  17. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffCRRemainder line 323
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCR_equation line 327
  19. def OAI.HigherDimensionalBallPacking.Rigidity.scalarDirection line 346
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.scalarDirection_smooth line 348
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.scalarDirection_support line 352
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.scalarDirection_norm line 358
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.scalarDirection_fderiv_norm line 362
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCRRemainder_smooth line 370
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCRRemainder_support line 378
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_direction_product_bounds line 385
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCRRemainder_bounds line 405
  28. def OAI.HigherDimensionalBallPacking.Rigidity.localSchauderBound line 465
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smallCR_schauder line 470