OAI/Analysis/MatrixSigning/Potential/StrictEpigraph.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Conic.add_mem_interior_cone line 17
2. lemma OAI.CurrentKS.Conic.smul_mem_interior_cone line 31
3. def OAI.CurrentKS.Conic.strictEpigraph line 45
4. lemma OAI.CurrentKS.Conic.strictEpigraph_open line 50
5. lemma OAI.CurrentKS.Conic.strictEpigraph_convex line 63
6. lemma OAI.CurrentKS.Conic.nonpos_of_bounded_ray line 85
7. theorem OAI.CurrentKS.Conic.multiplier_rule line 94