OAI/Analysis/Quantum/DimensionTen/QuadraticBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DimensionTen.Border.quadraticPairs line 10
2. def OAI.DimensionTen.Border.quadraticIndex line 13
3. lemma OAI.DimensionTen.Border.quadraticIndex_bijective line 16
4. def OAI.DimensionTen.Border.quadraticEquiv line 18
5. lemma OAI.DimensionTen.Border.low_quadratic line 20
6. lemma OAI.DimensionTen.Border.quadraticEval_low line 28
7. lemma OAI.DimensionTen.Border.quadraticCoeffs_ne line 36
8. lemma OAI.DimensionTen.Border.quadratic_zero_bound line 54