OAI/Geometry/BallPacking/Rigidity/CurveArea.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.realCurve line 14
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_smooth line 17
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_fderiv line 20
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_CR line 27
  5. def OAI.HigherDimensionalBallPacking.Rigidity.planarPullback line 35
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_smooth line 39
  7. def OAI.HigherDimensionalBallPacking.Rigidity.oneForm line 45
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.oneForm_smooth line 49
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_eq_extDeriv line 54
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_curl line 69
  11. def OAI.HigherDimensionalBallPacking.Rigidity.curveDensity line 88
  12. def OAI.HigherDimensionalBallPacking.Rigidity.curvePrimitive line 92
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.curvePrimitive_smooth line 95
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.curvePrimitive_curl line 99
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.curveDensity_smooth line 105
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.curveDensity_nonneg line 112
  17. def OAI.HigherDimensionalBallPacking.Rigidity.blowupSize line 133
  18. def OAI.HigherDimensionalBallPacking.Rigidity.blowupMoment line 135
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupMoment_smooth line 137
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupMoment_hasDerivAt line 140
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupMoment_before line 144
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupMoment_after line 148
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialOffset_sub_id_antitone line 155
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupMoment_ge_id line 163
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupSize_bounds line 171
  26. def OAI.HigherDimensionalBallPacking.Rigidity.blowupCoefficient line 178
  27. def OAI.HigherDimensionalBallPacking.Rigidity.blowupSlope line 180
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupCoefficient_smoothAt line 183
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupCoefficient_hasDerivAt line 187
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupCoefficient_before line 192
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupCoefficient_after line 196
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupSlope_nonpos line 200
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowup_radial_derivative line 207
  34. def OAI.HigherDimensionalBallPacking.Rigidity.weightedTwoForm line 213
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.weightedTwoForm_J_nonneg line 217
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupForm_J_nonneg line 228
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverse_chart_analyticAt line 239
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverse_chart_zero_iff line 254
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.not_locally_constant_in_chart line 266
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.isolated_chart_centre line 311
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.chart_centre_positive_order line 334
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.not_constant line 362
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.finite_centre_fibre line 373
  44. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_smul_complex line 391
  45. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_smul_complex_same line 396
  46. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_smul_complex_self line 404
  47. def OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive line 412
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_apply line 415
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_pos line 420
  50. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_smoothAt line 424
  51. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_smul line 429
  52. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_power line 445
  53. theorem OAI.HigherDimensionalBallPacking.Rigidity.complex_winding_eq_angular line 460
  54. def OAI.HigherDimensionalBallPacking.Rigidity.weightedPrimitive line 478
  55. theorem OAI.HigherDimensionalBallPacking.Rigidity.weightedPrimitive_smoothAt line 481
  56. theorem OAI.HigherDimensionalBallPacking.Rigidity.weightedPrimitive_differentiableAt line 487
  57. theorem OAI.HigherDimensionalBallPacking.Rigidity.weightedPrimitive_derivative line 493
  58. theorem OAI.HigherDimensionalBallPacking.Rigidity.weightedPrimitive_extDeriv line 505
  59. def OAI.HigherDimensionalBallPacking.Rigidity.blowupPrimitive line 527
  60. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupPrimitive_smoothAt line 530
  61. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupPrimitive_extDeriv line 534
  62. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupPrimitive_extDeriv_nonneg line 541
  63. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupPrimitive_before line 547
  64. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowupPrimitive_after line 556