OAI/LinearAlgebra/MatrixMultiplication/Numerical/AllFieldCertificates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Exact rational intervals, logarithm bounds and arithmetic circuit soundness.

  1. structure OAI.MatrixMultiplication.AllFieldCertificates.Ball line 11
  2. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.Encloses line 18
  3. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.exact line 20
  4. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.add line 21
  5. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.neg line 22
  6. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.mul line 23
  7. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.lower line 27
  8. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.upper line 28
  9. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.ofBounds line 30
  10. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.nonnegative_radius line 32
  11. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.bounds line 36
  12. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.ofBounds_sound line 42
  13. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.exact_sound line 49
  14. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.add_sound line 52
  15. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.neg_sound line 61
  16. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.mul_sound line 65
  17. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.widen_sound line 87
  18. def OAI.MatrixMultiplication.AllFieldCertificates.Ball.inv line 98
  19. theorem OAI.MatrixMultiplication.AllFieldCertificates.Ball.inv_sound line 100
  20. def OAI.MatrixMultiplication.AllFieldCertificates.reductionError line 113
  21. theorem OAI.MatrixMultiplication.AllFieldCertificates.reduction_error_cast line 116
  22. def OAI.MatrixMultiplication.AllFieldCertificates.logBall line 120
  23. theorem OAI.MatrixMultiplication.AllFieldCertificates.logBall_sound line 123
  24. theorem OAI.MatrixMultiplication.AllFieldCertificates.log_center_lipschitz line 139
  25. inductive OAI.MatrixMultiplication.AllFieldCertificates.Expression line 172
  26. def OAI.MatrixMultiplication.AllFieldCertificates.Expression.value line 180
  27. inductive OAI.MatrixMultiplication.AllFieldCertificates.Certificate line 188
  28. theorem OAI.MatrixMultiplication.AllFieldCertificates.Certificate.sound line 199
  29. theorem OAI.MatrixMultiplication.AllFieldCertificates.published_endpoint_below_target line 210
  30. theorem OAI.MatrixMultiplication.AllFieldCertificates.value_below_target_of_certificate line 214