OAI/Analysis/MatrixSigning/Potential/Point.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Variational.Point line 15
  2. def OAI.CurrentKS.Variational.domain line 17
  3. def OAI.CurrentKS.Variational.objective line 19
  4. def OAI.CurrentKS.Variational.residual line 21
  5. def OAI.CurrentKS.Variational.feasible line 25
  6. lemma OAI.CurrentKS.Variational.feasible_iff line 28
  7. lemma OAI.CurrentKS.Variational.continuous_objective line 35
  8. lemma OAI.CurrentKS.Variational.trace_bounds_of_feasible line 40
  9. lemma OAI.CurrentKS.Variational.objective_bounds line 56
  10. lemma OAI.CurrentKS.Variational.inverse_bounds line 66
  11. lemma OAI.CurrentKS.Variational.sublevel_box line 85