OAI/Geometry/PrescribedPotential/CircleRadialCalculus.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Circle Radial Calculus.

  1. def OAI.PotentialABP.v line 17
  2. def OAI.PotentialABP.w line 18
  3. lemma OAI.PotentialABP.dv line 20
  4. lemma OAI.PotentialABP.dw line 21
  5. lemma OAI.PotentialABP.cv line 24
  6. lemma OAI.PotentialABP.cw line 25
  7. def OAI.PotentialABP.circleIntegralReal line 28
  8. def OAI.PotentialABP.radialIntegral line 30
  9. def OAI.PotentialABP.secondRadialIntegral line 32
  10. def OAI.PotentialABP.angularHessianIntegral line 34
  11. lemma OAI.PotentialABP.circleIntegralReal_eq_circleAverage line 37
  12. lemma OAI.PotentialABP.circleIntegralReal_hasDerivAt line 46
  13. lemma OAI.PotentialABP.radialIntegral_hasDerivAt line 59
  14. lemma OAI.PotentialABP.radialIntegral_eq_radius_angular line 76
  15. lemma OAI.PotentialABP.radialIntegral_continuous line 111
  16. lemma OAI.PotentialABP.circleIntegralReal_continuous line 114
  17. lemma OAI.PotentialABP.hessian_circle_pair line 118
  18. theorem OAI.PotentialABP.smooth_circle_submean line 134