OAI/Geometry/BallPacking/Rigidity/Adapted.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_smooth_cutoff line 15
  2. def OAI.HigherDimensionalBallPacking.Rigidity.localizeJ line 30
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizeJ_compatible line 35
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizeJ_eq_standard line 44
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizeJ_smooth line 52
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.localizeJ_eqOn line 70
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.extend_two_compatible line 77
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.continuous_capacity line 155
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.closedBall_isClosed line 159
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.openBall_isOpen line 162
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.closedBall_isCompact line 165
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.adapt_two_ball_images line 184
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.packing_two_has_adapted_structure line 204
  14. def OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve line 233
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.pseudoHolomorphicAt_standard_of_complex line 238
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.standard_affine_line line 247
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.interpolateJ_standard line 264
  18. def OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy line 279
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_compatible line 282
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_smooth line 286
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_zero line 294
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_one line 298
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_support line 302
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_compact line 315
  25. def OAI.HigherDimensionalBallPacking.Rigidity.radialSwitch line 327
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSwitch_smooth line 329
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSwitch_nonneg line 332
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSwitch_le_one line 335
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSwitch_zero line 338
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSwitch_one line 343
  31. def OAI.HigherDimensionalBallPacking.Rigidity.radialOffset line 349
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialOffset_hasDerivAt line 351
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialOffset_smooth line 357
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialOffset_zero line 365
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialOffset_nonneg line 375
  36. def OAI.HigherDimensionalBallPacking.Rigidity.radialShift line 382
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialShift_pos line 384
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialOffset_after line 390
  39. def OAI.HigherDimensionalBallPacking.Rigidity.radialCoefficient line 407
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialCoefficient_pos line 409
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialCoefficient_smooth line 413
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialCoefficient_hasDerivAt line 418
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialCoefficient_one line 425
  44. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialCoefficient_after line 429
  45. def OAI.HigherDimensionalBallPacking.Rigidity.radialMoment line 433
  46. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_hasDerivAt line 435
  47. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_derivative_pos line 455
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_zero line 476
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_before line 479
  50. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_after line 483
  51. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_tendsto_one line 487