OAI/Geometry/BallPacking/Necessity/DensityExistence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointContinuation.LocallyPrecompact.comp_contDiffAt line 39
2. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseCoords_locallyPrecompact line 54
3. def OAI.HigherDimensionalBallPacking.Rigidity.responseFactor line 62
4. def OAI.HigherDimensionalBallPacking.Rigidity.densityResponse line 67
5. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseFactor_contDiffAt line 72
6. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResponse_contDiffAt line 80
7. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResponse_locallyPrecompact line 87
8. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseCoefficient_uncut line 113
9. theorem OAI.HigherDimensionalBallPacking.Rigidity.responseCoefficient_invertible line 126
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityFixedPoint_residual_zero line 159
11. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResponse_zero_time line 195
12. theorem OAI.HigherDimensionalBallPacking.Rigidity.actual_affine_line_exists line 232