OAI/Combinatorics/Progressions/Estimates/JointTupleTolerance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coefficientRowAccuracy line 13
  2. theorem OAI.Erdos3.coefficientRowAccuracy_pos line 15
  3. theorem OAI.Erdos3.coefficientRowAccuracy_sum line 18
  4. def OAI.Erdos3.scalarTupleToleranceCutoff line 25
  5. theorem OAI.Erdos3.scalarTupleToleranceCutoff_mono_modulus line 31
  6. theorem OAI.Erdos3.scalarTupleToleranceCutoff_le line 40
  7. theorem OAI.Erdos3.scalarTupleToleranceCutoff_mul line 49
  8. theorem OAI.Erdos3.scalarTupleToleranceCutoff_spec line 75
  9. theorem OAI.Erdos3.coefficientComparisonError_le line 108
  10. def OAI.Erdos3.coefficientToleranceScale line 121
  11. theorem OAI.Erdos3.coefficientToleranceScale_spec line 128
  12. def OAI.Erdos3.maskedProductAccuracy line 151
  13. theorem OAI.Erdos3.maskedProductAccuracy_pos line 154
  14. theorem OAI.Erdos3.maskedProductAccuracy_le_one line 160
  15. theorem OAI.Erdos3.maskedProductAccuracy_error line 169
  16. theorem OAI.Erdos3.maskedProductAccuracy_inverse_exp line 188
  17. theorem OAI.Erdos3.principalAxisTupleIndex_card_le line 229
  18. theorem OAI.Erdos3.scalarTupleToleranceCutoff_card_le line 243
  19. def OAI.Erdos3.maskedJointTupleBudget line 251
  20. theorem OAI.Erdos3.maskedJointTupleBudget_nonneg line 255
  21. theorem OAI.Erdos3.maskedJointTupleQuadrature_le line 263