OAI/Analysis/MatrixSigning/Machines/DirectedRounding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W19.directedRound line 9
  2. def OAI.KS.W19.roundingResidual line 12
  3. theorem OAI.KS.W19.directedRound_grid line 15
  4. theorem OAI.KS.W19.roundingResidual_nonneg line 19
  5. theorem OAI.KS.W19.roundingResidual_lt line 24
  6. theorem OAI.KS.W19.directedRound_decomposition line 29
  7. theorem OAI.KS.W19.abs_sub_sign_mul_nonneg line 33
  8. theorem OAI.KS.W19.roundingCoefficient_nonneg line 40
  9. theorem OAI.KS.W19.directedRound_cast line 45
  10. theorem OAI.KS.W19.directedRound_cast_decomposition line 54
  11. theorem OAI.KS.W19.roundingResidual_cast_bounds line 59
  12. theorem OAI.KS.W19.roundingCoefficient_cast_nonneg line 66