OAI/LinearAlgebra/MatrixMultiplication/Numerical/ComplexCertificates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact rational intervals, logarithm bounds and arithmetic circuit soundness.

  1. def OAI.MatrixMultiplication.ComplexCertificates.curveU line 12
  2. def OAI.MatrixMultiplication.ComplexCertificates.curveV line 13
  3. def OAI.MatrixMultiplication.ComplexCertificates.curveZ line 14
  4. def OAI.MatrixMultiplication.ComplexCertificates.curveG line 15
  5. def OAI.MatrixMultiplication.ComplexCertificates.curveH line 17
  6. theorem OAI.MatrixMultiplication.ComplexCertificates.curveU_cube line 19
  7. theorem OAI.MatrixMultiplication.ComplexCertificates.curveV_cube line 23
  8. theorem OAI.MatrixMultiplication.ComplexCertificates.curveU_bounds line 27
  9. theorem OAI.MatrixMultiplication.ComplexCertificates.curveV_bounds line 38
  10. theorem OAI.MatrixMultiplication.ComplexCertificates.curveZ_bounds line 49
  11. theorem OAI.MatrixMultiplication.ComplexCertificates.curveG_bounds line 68
  12. theorem OAI.MatrixMultiplication.ComplexCertificates.curveH_bounds line 98
  13. def OAI.MatrixMultiplication.ComplexCertificates.squareLeafCount line 110
  14. theorem OAI.MatrixMultiplication.ComplexCertificates.square_log_lower line 112