OAI/Geometry/BallPacking/Necessity/AffineEnergy.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.dirichletDensity line 37
  2. def OAI.HigherDimensionalBallPacking.Rigidity.complexDefect line 41
  3. def OAI.HigherDimensionalBallPacking.Rigidity.defectDensity line 44
  4. def OAI.HigherDimensionalBallPacking.Rigidity.standardCurvePrimitive line 47
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardCurvePrimitive_smooth line 50
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardCurvePrimitive_curl line 54
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_defect_identity line 62
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.dirichlet_defect_identity line 73
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.dirichletDensity_nonneg line 79
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.dirichletDensity_smooth line 82
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.defectDensity_smooth line 90
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerCutoff_integral_tendsto line 98
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerCutoff_integrable line 119
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.integrable_of_nonneg_of_outerCutoff_limit line 124
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.affine_remainder_extends line 167
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardCurvePrimitive_angular_limit_zero line 189
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_smooth line 204
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_affine_fderiv line 207
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.complexDefect_sub_affine line 216
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.defectDensity_sub_affine line 231
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_remainder_energy_identity line 237
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_joint_continuous line 278
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_self_smul line 300
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_defect_continuousOn line 305
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_radial_graph_continuousOn line 318
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_defect_unit_bound line 337
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_defect_bound line 375
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_affine_error_energy line 413