OAI/LinearAlgebra/MatrixMultiplication/Numerical/AllFieldCertificatesReplay.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Exact rational intervals, logarithm bounds and arithmetic circuit soundness.

  1. inductive OAI.MatrixMultiplication.AllFieldCertificates.Replay.Op line 11
  2. instance OAI.MatrixMultiplication.AllFieldCertificates.Replay.(instance at line 20) line 20
  3. abbrev OAI.MatrixMultiplication.AllFieldCertificates.Replay.Program line 29
  4. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.Op.value line 31
  5. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.Program.eval line 39
  6. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.contains line 42
  7. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.contains_sound line 45
  8. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.polynomial line 49
  9. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.traceHead line 53
  10. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkPolynomial line 55
  11. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkPolynomial_sound line 62
  12. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.logCoefficients line 79
  13. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.realApprox_eq_polynomial line 82
  14. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.normalized_log_error_48 line 91
  15. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.pad line 99
  16. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.pad_sound line 101
  17. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.logVariable line 112
  18. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.normalizedLogBall line 114
  19. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.normalizedLogBall_sound line 117
  20. structure OAI.MatrixMultiplication.AllFieldCertificates.Replay.LogWitness line 135
  21. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.logResult line 141
  22. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkLog line 145
  23. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkLog_sound line 151
  24. structure OAI.MatrixMultiplication.AllFieldCertificates.Replay.Witness line 170
  25. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.ballAt line 175
  26. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkStep line 177
  27. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.Related line 188
  28. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkStep_sound line 191
  29. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.Related.push line 210
  30. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.Related.empty line 220
  31. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.evalFrom line 226
  32. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.ballsFrom line 229
  33. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkFrom line 232
  34. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkFrom_sound line 238
  35. def OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkProgram line 254
  36. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkProgram_sound line 257
  37. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.evalFrom_append line 263
  38. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.ballsFrom_append line 267
  39. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checkFrom_append line 271
  40. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checked_upper_bound line 289
  41. theorem OAI.MatrixMultiplication.AllFieldCertificates.Replay.checked_below_target line 296