OAI/LinearAlgebra/MatrixMultiplication/Numerical/ComplexLogThreeCertificate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact rational intervals, logarithm bounds and arithmetic circuit soundness.

  1. theorem OAI.MatrixMultiplication.Foundation.log_three_upper line 10