OAI/Geometry/BallPacking/Necessity/PlanarEnergy.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.phaseEuclidean line 37
  2. def OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm line 40
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm_sq line 42
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm_nonneg line 48
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm_add_le line 50
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_abs_le line 54
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.standard_graph_energy_smul line 62
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.standard_graph_area_smul line 68
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_standard_graph_continuousOn line 73
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_standard_unit_bound line 104
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_standard_energy_bound line 128
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.interval_integral_sq_le line 165
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclidean_displacement_le_integral line 191
  14. def OAI.HigherDimensionalBallPacking.Rigidity.planarDirichlet line 204
  15. def OAI.HigherDimensionalBallPacking.Rigidity.horizontalSpeed line 208
  16. def OAI.HigherDimensionalBallPacking.Rigidity.verticalSpeed line 211
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.planar_partial_continuous line 214
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.euclideanNorm_continuous line 218
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.horizontalSpeed_continuous line 221
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.verticalSpeed_continuous line 226
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.horizontal_displacement_bound line 231
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.vertical_displacement_bound line 240
  23. def OAI.HigherDimensionalBallPacking.Rigidity.rectangleBoundaryLength line 249
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangleBoundaryLength_nonneg line 255
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.planar_stokes_rectangle line 264
  26. def OAI.HigherDimensionalBallPacking.Rigidity.translatedPlanarPrimitive line 301
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.translatedPlanarPrimitive_smooth line 304
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.translatedPlanarPrimitive_apply line 309
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.translatedPlanarPrimitive_curl line 317
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangle_boundary_displacement line 324
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.standard_area_rectangle_le_length_sq line 375
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarDirichlet_nonneg line 426
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarDirichlet_continuous line 429
  34. def OAI.HigherDimensionalBallPacking.Rigidity.rectangleBoundaryEnergy line 436
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.rectangleBoundaryLength_sq_le line 442
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.standard_area_rectangle_le_boundaryEnergy line 497