OAI/Analysis/MatrixSigning/Optimization/UpperIndex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalGrid.upperIndex line 11
2. def OAI.CurrentKS.RationalGrid.upper line 15
3. lemma OAI.CurrentKS.RationalGrid.upperIndex_le line 17
4. lemma OAI.CurrentKS.RationalGrid.upperIndex_spec line 26
5. theorem OAI.CurrentKS.RationalGrid.upper_spec line 44
6. def OAI.CurrentKS.RationalSDP.rationalVariance line 74
7. def OAI.CurrentKS.RationalSDP.varianceTest line 78
8. def OAI.CurrentKS.RationalSDP.varianceQuery line 81
9. lemma OAI.CurrentKS.RationalSDP.rationalVariance_symm line 88
10. lemma OAI.CurrentKS.RationalSDP.rationalVariance_cast line 96
11. lemma OAI.CurrentKS.RationalSDP.varianceTest_spec line 108
12. theorem OAI.CurrentKS.RationalSDP.varianceQuery_spec line 122