OAI/Geometry/BallPacking/Degree/BoxContinuation.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.finite_box_continuation line 14
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.compact_smooth_plateau line 72
  3. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.finiteTimeFreeze line 93
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.finiteTimeFreeze_smooth line 97
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.finiteTimeFreeze_zero line 106
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.finiteTimeFreeze_one line 110
  7. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.cutoffPullTopForm line 121
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.tail_smooth line 127
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.cutoffPullTopForm_differentiable line 130
  10. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.extDeriv_constant_zero line 137
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.cutoffPullTopForm_closed line 143
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.separating_bump_support line 168
  13. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.tailCLM line 189
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.tailCLM_apply line 191
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.tail_coordinate_zero line 192
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.tail_coordinate_succ line 195
  17. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm line 199
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_smooth line 203
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_flux_zero line 207
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_flux_other line 214
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_exterior_basis line 225
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_zero_of_time line 248
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_zero_of_space line 251
  24. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise line 261
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_smooth line 262
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_initial line 265
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_final line 267
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_monotone line 269
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_deriv_nonneg line 272
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_deriv_zero line 274
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_deriv_support line 287
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarRise_deriv_positive line 292
  33. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarCutoff line 299
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarCutoff_smooth line 300
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarCutoff_deriv line 302
  36. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarCutoff_zero line 306
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarCutoff_deriv_initial line 312
  38. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarCutoff_deriv_support line 315
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.topForm_eq_zero_of_basis line 332
  40. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collarVolumeForm_exterior_zero line 344
  41. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collar_pullback_density line 356
  42. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collar_pullback_exterior_supported line 365
  43. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.collar_pullback_identity_density line 373
  44. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.chartedSpace line 393
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.isManifold line 400
  46. lemma OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.secondCountable line 411
  47. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.partition_exists line 416
  48. def OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.restrict line 439
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.Degree.SignedSmoothAtlas.finite_neighborhood line 482