OAI/Geometry/BallPacking/Rigidity/Correction.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HigherDimensionalBallPacking.Rigidity.stdPrimitive line 13
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdPrimitive_smooth line 16
  3. def OAI.HigherDimensionalBallPacking.Rigidity.inversePullback line 19
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.inversePullback_smoothAt line 23
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverse_fderiv_preserves_form line 32
  6. def OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection line 44
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_eq_near line 50
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_zero_off line 58
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_support line 75
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_compact line 85
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_zero_near line 93
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_smoothAt line 103
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.complex_power_fderiv_real line 125
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.power_curve_fderiv line 131
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_power_pullback line 140
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_branch_residue line 164
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_smoothAt line 199
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_smoothAt line 204
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_zero line 210
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_remainder_smooth line 213
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowup_branch_residue line 222
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.oneForm_smoothAt line 271
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.oneForm_extDeriv_apply line 276
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.oneForm_extDeriv_sub line 290
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.oneForm_extDeriv_add line 299
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.oneForm_extDeriv_congr line 308
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_eq_extDeriv_at line 313
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_curlAt line 318
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.inversePullback_extDeriv line 336
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.stdPrimitive_extDeriv line 356
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_extDeriv line 362
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.inverse_fderiv_intertwines line 380
  33. def OAI.HigherDimensionalBallPacking.Rigidity.planeRotation line 398
  34. def OAI.HigherDimensionalBallPacking.Rigidity.outerProfile line 400
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_smooth line 403
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_compact line 408
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_nonneg line 417
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_zero_value line 420
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_deriv line 425
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_deriv_nonpos line 440
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_deriv_zero_before line 445
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffWedge_radial_rotation line 454
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.nonneg_angular_limit_of_nonneg_curl line 469