OAI/Analysis/MatrixSigning/Optimization/SquareInterval.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalRoot.squareInterval line 9
2. lemma OAI.CurrentKS.RationalRoot.squareInterval_spec line 16
3. lemma OAI.CurrentKS.RationalRoot.squareInterval_upper_error line 51
4. lemma OAI.CurrentKS.RationalRoot.inverse_pow_size_le line 62
5. def OAI.CurrentKS.RationalRoot.upperSqrt line 73
6. theorem OAI.CurrentKS.RationalRoot.upperSqrt_spec line 75