OAI/Analysis/MatrixSigning/Arithmetic/CubeInterval.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Scalar.cubeInterval line 10
2. lemma OAI.CurrentKS.Scalar.cubeInterval_spec line 17
3. lemma OAI.CurrentKS.Scalar.cubeInterval_error line 52
4. lemma OAI.CurrentKS.Scalar.cubeInterval_lower_mem line 63
5. lemma OAI.CurrentKS.Scalar.psi_closed_cube line 68
6. lemma OAI.CurrentKS.Scalar.psi_closed_bounds line 74
7. def OAI.CurrentKS.Scalar.approxPsi line 84
8. lemma OAI.CurrentKS.Scalar.inverse_pow_size_le line 86
9. lemma OAI.CurrentKS.Scalar.approxPsi_spec line 97