OAI/Geometry/PrescribedPotential/ContactSetABP.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Contact Set A B P.

  1. def OAI.PotentialABP.contacts line 21
  2. lemma OAI.PotentialABP.gradient_continuous line 25
  3. lemma OAI.PotentialABP.contacts_isClosed line 30
  4. lemma OAI.PotentialABP.contacts_sublevel line 45
  5. lemma OAI.PotentialABP.contacts_interior line 55
  6. lemma OAI.PotentialABP.tilted_minimum_gradient line 66
  7. lemma OAI.PotentialABP.gradient_image_contacts line 87
  8. lemma OAI.PotentialABP.gradient_contDiff line 122
  9. lemma OAI.PotentialABP.contact_measure_estimate line 129
  10. lemma OAI.PotentialABP.contacts_hessian_nonneg line 149