OAI/LinearAlgebra/MatrixMultiplication/Numerical/ComplexCertificatesLog.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Exact rational intervals, logarithm bounds and arithmetic circuit soundness.

  1. theorem OAI.MatrixMultiplication.ComplexCertificates.log_bounds_of_reduction line 12
  2. def OAI.MatrixMultiplication.ComplexCertificates.reduceTwo line 23
  3. theorem OAI.MatrixMultiplication.ComplexCertificates.log_two_bounds line 30
  4. def OAI.MatrixMultiplication.ComplexCertificates.reduceThree line 37
  5. theorem OAI.MatrixMultiplication.ComplexCertificates.log_three_lower line 44
  6. theorem OAI.MatrixMultiplication.ComplexCertificates.log_three_upper line 50
  7. def OAI.MatrixMultiplication.ComplexCertificates.reduceNineteen line 55
  8. theorem OAI.MatrixMultiplication.ComplexCertificates.log_nineteen_bounds line 62
  9. def OAI.MatrixMultiplication.ComplexCertificates.reduceCurveLo line 69
  10. def OAI.MatrixMultiplication.ComplexCertificates.reduceCurveHi line 76
  11. theorem OAI.MatrixMultiplication.ComplexCertificates.log_curve_lower line 83
  12. theorem OAI.MatrixMultiplication.ComplexCertificates.log_curve_upper line 90
  13. def OAI.MatrixMultiplication.ComplexCertificates.reduceTen line 97
  14. theorem OAI.MatrixMultiplication.ComplexCertificates.log_ten_lower line 104
  15. def OAI.MatrixMultiplication.ComplexCertificates.reduceSquareMantissa line 110
  16. theorem OAI.MatrixMultiplication.ComplexCertificates.log_square_mantissa_lower line 117
  17. def OAI.MatrixMultiplication.ComplexCertificates.reduceNineSevenths line 124
  18. theorem OAI.MatrixMultiplication.ComplexCertificates.log_nine_sevenths_bounds line 131
  19. def OAI.MatrixMultiplication.ComplexCertificates.reduceExpLo48 line 138
  20. theorem OAI.MatrixMultiplication.ComplexCertificates.exp_neg_354_lower line 145
  21. def OAI.MatrixMultiplication.ComplexCertificates.reduceExpHi48 line 152
  22. theorem OAI.MatrixMultiplication.ComplexCertificates.exp_neg_348_upper line 159
  23. def OAI.MatrixMultiplication.ComplexCertificates.reduceExpLo288 line 166
  24. theorem OAI.MatrixMultiplication.ComplexCertificates.exp_neg_86_lower line 173
  25. def OAI.MatrixMultiplication.ComplexCertificates.reduceZ48Lo line 180
  26. def OAI.MatrixMultiplication.ComplexCertificates.reduceZ48Hi line 187
  27. theorem OAI.MatrixMultiplication.ComplexCertificates.log_z48_lower line 194
  28. theorem OAI.MatrixMultiplication.ComplexCertificates.log_z48_upper line 201
  29. def OAI.MatrixMultiplication.ComplexCertificates.reduceZ288Lo line 208
  30. theorem OAI.MatrixMultiplication.ComplexCertificates.log_z288_lower line 215