OAI/Geometry/BallPacking/Rigidity/RadialForm.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_standardForm_sq_le line 12
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdDot_J_right line 43
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_eq_stdDot line 47
  4. def OAI.HigherDimensionalBallPacking.Rigidity.radialSlope line 52
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSlope_nonpos line 55
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialSlope_zero line 58
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialMoment_derivative_eq line 61
  8. def OAI.HigherDimensionalBallPacking.Rigidity.radialForm line 70
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_standard line 75
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_J_pos line 81
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_adapted_pos line 94
  12. def OAI.HigherDimensionalBallPacking.Rigidity.stdOmega line 104
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdOmega_apply line 107
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_smooth line 112
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_hasFDerivAt line 119
  16. def OAI.HigherDimensionalBallPacking.Rigidity.radialPrimitiveCLM line 138
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialPrimitiveCLM_smooth line 141
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialPrimitiveCLM_derivative line 146
  19. def OAI.HigherDimensionalBallPacking.Rigidity.radialPrimitive line 163
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialPrimitive_smooth line 166
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_extDeriv line 171
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_closed line 191
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.linear_asymptotic_norm_tendsto line 196
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.tendsto_cocompact line 210
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.isProperMap line 217
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.holomorphic_at_infinity line 221
  27. def OAI.HigherDimensionalBallPacking.Rigidity.infinityGerm line 232
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.infinityGerm_eventuallyEq line 235
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.infinityGerm_analyticAt line 241
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.analytic_at_infinity line 267
  31. abbrev OAI.SymplecticBallPacking.Hamiltonian.Plane line 281
  32. def OAI.SymplecticBallPacking.Hamiltonian.planarArea line 283
  33. theorem OAI.SymplecticBallPacking.Hamiltonian.planarArea_apply line 289
  34. def OAI.SymplecticBallPacking.Hamiltonian.planarCurl line 290
  35. def OAI.SymplecticBallPacking.Hamiltonian.radiusSq line 292
  36. theorem OAI.SymplecticBallPacking.Hamiltonian.radiusSq_nonneg line 293
  37. theorem OAI.SymplecticBallPacking.Hamiltonian.radiusSq_smooth line 296
  38. theorem OAI.SymplecticBallPacking.Hamiltonian.radiusSq_polar line 298
  39. theorem OAI.SymplecticBallPacking.Hamiltonian.HasCompactSupport.left_slice line 302
  40. theorem OAI.SymplecticBallPacking.Hamiltonian.HasCompactSupport.right_slice line 309
  41. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_compact_partial_fst line 316
  42. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_compact_partial_snd line 337
  43. theorem OAI.SymplecticBallPacking.Hamiltonian.compact_planar_stokes line 358
  44. theorem OAI.SymplecticBallPacking.Hamiltonian.HasCompactSupport.comp_radiusSq line 385
  45. theorem OAI.SymplecticBallPacking.Hamiltonian.HasCompactSupport.comp_square line 398
  46. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_radial_derivative line 403
  47. def OAI.SymplecticBallPacking.Hamiltonian.planarDot line 429
  48. theorem OAI.SymplecticBallPacking.Hamiltonian.planarDot_apply line 435
  49. theorem OAI.SymplecticBallPacking.Hamiltonian.radiusSq_hasFDerivAt line 437
  50. def OAI.SymplecticBallPacking.Hamiltonian.angularOneForm line 449
  51. theorem OAI.SymplecticBallPacking.Hamiltonian.angularOneForm_contDiffAt line 451
  52. theorem OAI.SymplecticBallPacking.Hamiltonian.radialArea_curl line 455
  53. theorem OAI.SymplecticBallPacking.Hamiltonian.cutoffAngular_curl line 470
  54. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_cutoffAngular_density line 485