OAI/Analysis/MatrixSigning/Optimization/ValueObjectiveCoeffs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalSDP.valueObjectiveCoeffs line 16
2. def OAI.CurrentKS.RationalSDP.valueLipschitz line 21
3. lemma OAI.CurrentKS.RationalSDP.valueObjectiveCoeffs_dot line 23
4. lemma OAI.CurrentKS.RationalSDP.valueObjectiveCoeffs_real line 29
5. lemma OAI.CurrentKS.RationalSDP.objectiveCLM_value line 50
6. lemma OAI.CurrentKS.RationalSDP.valueObjectiveCoeffs_bound line 57
7. lemma OAI.CurrentKS.RationalSDP.valueLipschitz_pos line 83
8. lemma OAI.CurrentKS.RationalSDP.objectiveCLM_value_norm line 87