OAI/LinearAlgebra/MatrixMultiplication/Numerical/AllFieldCertificatesReplayStatic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact rational intervals, logarithm bounds and arithmetic circuit soundness.

  1. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.Op.before line 9
  2. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkOp line 17
  3. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkOp_sound line 28
  4. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkAt line 54
  5. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkRange line 57
  6. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkRange_at line 62
  7. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkRange_append line 79
  8. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkedValues_sound line 92
  9. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.RangeChecked line 109
  10. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.rangeChecked_of_checkRange line 112
  11. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.RangeChecked.join line 120