OAI/Analysis/StrictMeans/SquaredPotential.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.squaredReciprocalPotential line 11
  2. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_contDiffAt line 14
  3. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_eq_exp line 20
  4. lemma OAI.StrictInverseFirstPower.logPotential_contDiffAt line 32
  5. lemma OAI.StrictInverseFirstPower.realHessian_exp line 39
  6. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_hessian line 59
  7. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_laplacian_pos_off_pole line 100
  8. lemma OAI.StrictInverseFirstPower.realHessian_mul line 119
  9. lemma OAI.StrictInverseFirstPower.realHessian_norm_sq_at_zero line 148
  10. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_fderiv_pole line 166
  11. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_hessian_pole line 178
  12. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_laplacian_pos line 200