OAI/Geometry/BallPacking/Necessity/DensityMaps.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCurve_deriv_one line 53
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCurve_C1_curl line 62
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCurve_regular line 78
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCurve_affineLine line 100
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResidual_zero_affineLine line 109
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCurve_lower_bound line 139
  7. def OAI.HigherDimensionalBallPacking.Rigidity.goodDensities line 156
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.goodDensities_isOpen line 159
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.goodDensities_slope_ne line 163
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.goodDensities_exterior line 167
  11. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffValues line 197
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffValues_value line 202
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffValues_compact line 206
  14. abbrev OAI.HigherDimensionalBallPacking.Rigidity.ResponseCoords line 213
  15. def OAI.HigherDimensionalBallPacking.Rigidity.responseCoords line 215
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseCoords_contDiff line 219
  17. def OAI.HigherDimensionalBallPacking.Rigidity.responseProfile line 228
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseProfile_contDiff line 233
  19. def OAI.HigherDimensionalBallPacking.Rigidity.responseCoefficient line 245
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseCoefficient_contDiff line 250
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseCoefficient_value line 256