OAI/Analysis/MatrixSigning/Optimization/ObjectiveCLM.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.RationalSDP.Pencil.realEval_convex line 16
2. lemma OAI.CurrentKS.RationalSDP.Pencil.convex_feasible line 26
3. def OAI.CurrentKS.RationalSDP.objectiveCLM line 32
4. lemma OAI.CurrentKS.RationalSDP.objectiveCLM_apply line 35
5. lemma OAI.CurrentKS.RationalSDP.norm_convexCombination_le line 42
6. def OAI.CurrentKS.RationalSDP.nearRadius line 54
7. def OAI.CurrentKS.RationalSDP.optimizeFuel line 56
8. lemma OAI.CurrentKS.RationalSDP.nearRadius_pos line 58
9. lemma OAI.CurrentKS.RationalSDP.nearRadius_le line 63
10. lemma OAI.CurrentKS.RationalSDP.exists_near_level line 68
11. theorem OAI.CurrentKS.RationalSDP.Pencil.optimize_nearOptimal line 90