OAI/Geometry/BallPacking/Necessity/DensityResidual.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.contDiffAt_interpolateJ_of_invertible line 39
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_coefficient_extension line 58
  3. def OAI.HigherDimensionalBallPacking.Rigidity.densityLinearSlope line 138
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityLinearSlope_apply line 143
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.densitySlope_contDiff line 147
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityLinearSlope_contDiff line 154
  7. def OAI.HigherDimensionalBallPacking.Rigidity.timeDensityProfile line 159
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.timeDensityProfile_contDiff line 167
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.timeDensityProfile_value line 185
  10. def OAI.HigherDimensionalBallPacking.Rigidity.densityCoefficient line 200
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCoefficient_value line 205
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCoefficient_contDiffAt line 211
  13. def OAI.HigherDimensionalBallPacking.Rigidity.densityJet line 223
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityJet_contDiff line 228
  15. def OAI.HigherDimensionalBallPacking.Rigidity.densityResidual line 234
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.holderApply_contDiffAt line 240
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityDerivativeOne_contDiff line 249
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactDensity_smooth line 256
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResidual_contDiffAt line 262
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityCurve_eq_profile line 270
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityJet_value line 281
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResidual_value line 289
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.pseudoHolomorphicAt_of_scalarCR line 305
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResidual_zero_iff line 321
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.densityResidual_at_zero_time line 350