OAI/MathematicalPhysics/CriticalSK/Saddle.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.saddleSum line 35
  2. lemma OAI.CriticalSK.saddleSum_strictAnti line 37
  3. theorem OAI.CriticalSK.spherical_saddle_existsUnique line 51
  4. def OAI.CriticalSK.sphericalObjective line 110
  5. lemma OAI.CriticalSK.log_tangent_bound line 113
  6. lemma OAI.CriticalSK.log_tangent_strict line 120
  7. theorem OAI.CriticalSK.spherical_saddle_strict_min line 130
  8. lemma OAI.CriticalSK.spherical_saddle_min line 162
  9. lemma OAI.CriticalSK.spherical_saddle_upper line 173
  10. lemma OAI.CriticalSK.spherical_saddle_lower line 192
  11. theorem OAI.CriticalSK.spherical_saddle_variance_bounds line 212