OAI/NumberTheory/PiExponent/Approximation/MatrixTranslationBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.MatrixTranslationBounds.weight line 12
  2. theorem OAI.PiExponent.MatrixTranslationBounds.error_power_product_le line 15
  3. theorem OAI.PiExponent.MatrixTranslationBounds.norm_rowScalar_exp_basic line 25
  4. theorem OAI.PiExponent.MatrixTranslationBounds.sum_exponents_le line 46
  5. theorem OAI.PiExponent.MatrixTranslationBounds.residual_exponent_identity line 60
  6. theorem OAI.PiExponent.MatrixTranslationBounds.norm_rowScalar_exp_weighted line 72
  7. theorem OAI.PiExponent.MatrixTranslationBounds.weight_sub_le_weight_tsub line 112
  8. theorem OAI.PiExponent.MatrixTranslationBounds.norm_rowScalar_exp_weight_difference line 126
  9. theorem OAI.PiExponent.MatrixTranslationBounds.actual_error_exp line 145
  10. def OAI.PiExponent.MatrixTranslationBounds.truncationOrder line 159
  11. theorem OAI.PiExponent.MatrixTranslationBounds.truncationOrder_pos line 161
  12. theorem OAI.PiExponent.MatrixTranslationBounds.truncationOrder_budget line 165