OAI/Geometry/BallPacking/Cauchy/GreenFormula.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SymplecticBallPacking.Hamiltonian.plane_deriv_first line 13
  2. theorem OAI.SymplecticBallPacking.Hamiltonian.plane_deriv_second line 18
  3. def OAI.SymplecticBallPacking.Hamiltonian.pullbackForm line 23
  4. theorem OAI.SymplecticBallPacking.Hamiltonian.bilinear_skew_plane line 26
  5. theorem OAI.SymplecticBallPacking.Hamiltonian.pullbackForm_smooth line 35
  6. theorem OAI.SymplecticBallPacking.Hamiltonian.pullbackForm_curl line 40
  7. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_curl_rectangle line 61
  8. theorem OAI.SymplecticBallPacking.Hamiltonian.polar_smooth line 92
  9. theorem OAI.SymplecticBallPacking.Hamiltonian.polar_deriv_first line 96
  10. theorem OAI.SymplecticBallPacking.Hamiltonian.polar_deriv_second line 101
  11. theorem OAI.SymplecticBallPacking.Hamiltonian.polar_area line 106
  12. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_curl_polar_rectangle line 113
  13. def OAI.SymplecticBallPacking.Hamiltonian.roundDisk line 138
  14. theorem OAI.SymplecticBallPacking.Hamiltonian.polar_mem_roundDisk line 140
  15. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_roundDisk_polar line 149
  16. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_curl_roundDisk line 181
  17. def OAI.SymplecticBallPacking.Hamiltonian.coordinateForm line 189
  18. theorem OAI.SymplecticBallPacking.Hamiltonian.coordinateForm_apply line 192
  19. theorem OAI.SymplecticBallPacking.Hamiltonian.coordinateForm_smooth line 195
  20. theorem OAI.SymplecticBallPacking.Hamiltonian.coordinateForm_compact line 199
  21. theorem OAI.SymplecticBallPacking.Hamiltonian.form_eval_fderiv line 207
  22. theorem OAI.SymplecticBallPacking.Hamiltonian.coordinateForm_curl line 213
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.polar_complex_eq_circleMap line 231
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.angular_complex_eq_circleMap line 236
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.roundDisk_measurable line 242
  26. def OAI.HigherDimensionalBallPacking.Rigidity.cauchyCurl line 245
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyCurl_smooth line 248
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyCurl_compact line 253
  29. def OAI.HigherDimensionalBallPacking.Rigidity.projectedCauchyForm line 258
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.projectedCauchyForm_smooth line 262
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.projectedCauchyForm_compact line 268
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.projectedCauchyForm_apply line 274
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.projectedCauchyForm_curl line 284
  34. theorem OAI.HigherDimensionalBallPacking.Rigidity.complex_compact_stokes line 306
  35. theorem OAI.HigherDimensionalBallPacking.Rigidity.complex_disk_stokes line 320
  36. def OAI.HigherDimensionalBallPacking.Rigidity.cauchyInnerBump line 343
  37. def OAI.HigherDimensionalBallPacking.Rigidity.cauchyPuncture line 349
  38. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyPuncture_compact line 352
  39. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyPuncture_smooth line 358
  40. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyPuncture_eventuallyEq line 370
  41. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyCurl_div line 379
  42. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyPuncture_curl line 393
  43. theorem OAI.HigherDimensionalBallPacking.Rigidity.complexCartesian_norm_sq line 402
  44. theorem OAI.HigherDimensionalBallPacking.Rigidity.complexCartesian_norm_ge_of_notMem line 407
  45. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchy_exterior_integral line 415
  46. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyCurl_div_integrable line 454
  47. theorem OAI.HigherDimensionalBallPacking.Rigidity.shrinking_exterior_aecover line 460
  48. theorem OAI.HigherDimensionalBallPacking.Rigidity.circle_mean_integral_limit line 477
  49. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchy_green_fundamental line 492
  50. def OAI.HigherDimensionalBallPacking.Rigidity.curlJet line 522
  51. lemma OAI.HigherDimensionalBallPacking.Rigidity.curlJet_apply line 526
  52. lemma OAI.HigherDimensionalBallPacking.Rigidity.curlJet_smul line 530
  53. lemma OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_zero line 534
  54. lemma OAI.HigherDimensionalBallPacking.Rigidity.regularizedCauchyJet_zero_fderiv line 539
  55. lemma OAI.HigherDimensionalBallPacking.Rigidity.regularizedCauchyJet_curl_zero line 561
  56. lemma OAI.HigherDimensionalBallPacking.Rigidity.cancellationJetIntegrand_integrable line 570
  57. def OAI.HigherDimensionalBallPacking.Rigidity.bumpCurlKernel line 591
  58. lemma OAI.HigherDimensionalBallPacking.Rigidity.bump_complex_smooth line 594
  59. lemma OAI.HigherDimensionalBallPacking.Rigidity.bump_complex_compact line 597
  60. lemma OAI.HigherDimensionalBallPacking.Rigidity.bumpCurlKernel_apply line 600
  61. lemma OAI.HigherDimensionalBallPacking.Rigidity.bumpCurlKernel_integrable line 608
  62. lemma OAI.HigherDimensionalBallPacking.Rigidity.bumpCurlKernel_integral line 611
  63. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyJet_curl line 616
  64. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyJet_curl line 623
  65. lemma OAI.HigherDimensionalBallPacking.Rigidity.curlJet_smulComp line 632
  66. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyDerivative_curl line 637
  67. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailIntegralJet_integrable line 649
  68. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyDerivative_curl line 655
  69. lemma OAI.HigherDimensionalBallPacking.Rigidity.bumpCurlKernel_smul_integrable line 665
  70. lemma OAI.HigherDimensionalBallPacking.Rigidity.globalCauchyDerivative_curl line 678
  71. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_curl line 694