OAI/Geometry/PrescribedPotential/SmoothPotentialDifference.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth Potential Difference.

  1. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.addFunction line 18
  2. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_addFunction line 22
  3. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.difference line 34
  4. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.difference_value line 37
  5. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_difference line 42