OAI/Geometry/BallPacking/Rigidity/AngularPoles.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_congr line 14
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_sub line 18
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_const_smul line 24
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_sum line 31
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarCurl_translate line 38
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.angularOneForm_curl line 45
  7. def OAI.HigherDimensionalBallPacking.Rigidity.angularPole line 49
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.angularPole_smoothAt line 51
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.angularPole_curl line 55
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.angularOneForm_rotation line 61
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.angularPole_tendsto_fixed line 67
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.angularPole_tendsto_rotation line 86
  13. def OAI.HigherDimensionalBallPacking.Rigidity.poleSum line 101
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.poleSum_smoothAt line 104
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.poleSum_curl line 110
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.poleSum_tendsto_rotation line 120
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.smooth_fill_finite line 128
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.finite_residues_le_infinity line 158
  19. theorem OAI.HigherDimensionalBallPacking.Rigidity.realCurve_translate line 222
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_translate line 227
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.tendsto_sub_punctured line 232
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.blowup_branch_residue_at line 242
  23. def OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive line 280
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive_smoothAt line 285
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.chartCorrection_extDeriv_zero line 295
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive_extDeriv line 305
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.radialForm_adapted_nonneg line 323
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive_extDeriv_nonneg line 332
  29. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedCurve_curl_nonneg line 372
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.inversePullback_sub line 397
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive_centre_remainder line 403
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_inverse line 435
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.planarPullback_add line 449
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.correctedPrimitive_centre_residue line 454
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.complex_inv_fderiv_real line 504
  36. theorem OAI.HigherDimensionalBallPacking.Rigidity.infinity_curve_fderiv line 510
  37. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_infinity_curve line 527
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.infinityGerm_curve_eventuallyEq line 537
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_infinity_limit line 544
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.equivRealProd_rotation line 584