OAI/Geometry/BallPacking/Necessity/SquareBounds.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.planeSquare line 37
  2. def OAI.HigherDimensionalBallPacking.Rigidity.squareEnergy line 40
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeSquare_compact line 43
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeSquare_mono line 45
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareEnergy_nonneg line 50
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareEnergy_mono line 53
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangle_integral_eq_iterated line 58
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangle_integral_eq_iterated_swap line 67
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_interval_mean line 78
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.horizontal_integral_continuous line 87
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.vertical_integral_continuous line 92
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.planar_energy_rectangle_bound line 97
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_low_energy_rectangle line 118
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.square_energy_hole_filling line 201
  15. def OAI.HigherDimensionalBallPacking.Rigidity.decayRatio line 221
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.decayRatio_nonneg line 223
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.decayRatio_lt_one line 226
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.square_energy_decay_half line 231
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.square_energy_decay_dyadic line 243
  20. def OAI.HigherDimensionalBallPacking.Rigidity.lineMean line 270
  21. def OAI.HigherDimensionalBallPacking.Rigidity.rectangleMean line 272
  22. def OAI.HigherDimensionalBallPacking.Rigidity.squareMean line 275
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_const line 278
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_sub line 283
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_mono line 287
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_abs_le line 294
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_lineMean_eq line 300
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_horizontal_continuous line 308
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_vertical_continuous line 312
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangleMean_eq_integral line 316
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangleMean_swap line 322
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.real_displacement_le_integral line 328
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.real_displacement_le_integral_outer line 335
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_oscillation line 346
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangle_integral_sq_le line 358
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.square_integral_abs_le line 373
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_half_bound line 398
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_squareMean_eq line 465
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.planeSquare_dist_le line 474
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_tendsto line 480
  41. def OAI.HigherDimensionalBallPacking.Rigidity.morreyConstant line 491
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.morreyConstant_pos line 493
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_point_bound line 499
  44. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_translate_bound line 552
  45. def OAI.HigherDimensionalBallPacking.Rigidity.phaseProjection line 655
  46. theorem OAI.HigherDimensionalBallPacking.Rigidity.phaseProjection_self line 658
  47. theorem OAI.HigherDimensionalBallPacking.Rigidity.phaseProjection_sq_le line 666
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_abs_le line 682
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_point_bound line 688
  50. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_translate_bound line 713
  51. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_add line 743
  52. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_add line 747
  53. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_sub line 757
  54. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineMean_linear line 767
  55. theorem OAI.HigherDimensionalBallPacking.Rigidity.squareMean_affine_scalar line 777
  56. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_affine_eq line 785
  57. theorem OAI.HigherDimensionalBallPacking.Rigidity.projection_squareMean_affine line 792