OAI/Analysis/SymmetricDomains/LocalMaxGraphParameter.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.exists_complex_parameter_conormal line 34
  2. def OAI.Release061.graphCriticalParameter line 59
  3. theorem OAI.Release061.graphCriticalParameter_iff line 63
  4. def OAI.Release061.graphCriticalEquiv line 82
  5. theorem OAI.Release061.differentiableAt_graphCriticalParameter line 95
  6. def OAI.Release061.selfDualGraphParameter line 105
  7. theorem OAI.Release061.differentiableAt_selfDualGraphParameter line 109
  8. theorem OAI.Release061.graph_weight_hasFDerivAt line 116
  9. theorem OAI.Release061.localMax_graph_parameter line 123