OAI/Analysis/StrictMeans/IndexGeometry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.nonsingular_locally_injective line 11
  2. lemma OAI.StrictInverseFirstPower.compact_level_regular_fiber_finite line 25
  3. def OAI.StrictInverseFirstPower.criticalCut line 54
  4. lemma OAI.StrictInverseFirstPower.goodPair_criticalCut_finite line 57
  5. def OAI.StrictInverseFirstPower.maximaCut line 73
  6. def OAI.StrictInverseFirstPower.saddleCut line 76
  7. lemma OAI.StrictInverseFirstPower.maximaCut_finite line 79
  8. lemma OAI.StrictInverseFirstPower.saddleCut_finite line 83
  9. def OAI.StrictInverseFirstPower.realHessian line 95
  10. lemma OAI.StrictInverseFirstPower.logPotential_hessian line 98
  11. lemma OAI.StrictInverseFirstPower.logPotential_hessian_trace line 124
  12. lemma OAI.StrictInverseFirstPower.critical_logarithmic_quotient_deriv line 132
  13. lemma OAI.StrictInverseFirstPower.logPotential_critical_hessian line 143
  14. lemma OAI.StrictInverseFirstPower.logPotential_hessian_det line 163
  15. lemma OAI.StrictInverseFirstPower.log_tangent_bound line 184
  16. lemma OAI.StrictInverseFirstPower.log_tangent_strict line 191
  17. lemma OAI.StrictInverseFirstPower.logPotential_not_isLocalMin line 199
  18. lemma OAI.StrictInverseFirstPower.compact_strict_maximum_principle line 268
  19. lemma OAI.StrictInverseFirstPower.reciprocal_logPotential_not_isLocalMax line 290
  20. lemma OAI.StrictInverseFirstPower.reciprocal_potential_inside_boundary line 309