OAI/Combinatorics/Progressions/Dynamics/PhysicalBadProductErrorBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_residue_error_le_of_common_gap line 11
  2. theorem OAI.Erdos3.finite_residue_error_common_gap_budget line 28
  3. def OAI.Erdos3.physicalBadProductAccuracy line 38
  4. theorem OAI.Erdos3.physicalBadProductAccuracy_pos line 41
  5. theorem OAI.Erdos3.physicalBadProductAccuracy_inv line 44
  6. theorem OAI.Erdos3.exp_eight_ge line 49
  7. theorem OAI.Erdos3.physicalBadProductAccuracy_budget line 58
  8. def OAI.Erdos3.physicalBadProductGap line 102
  9. theorem OAI.Erdos3.physicalBadProductGap_budget line 106
  10. theorem OAI.Erdos3.physicalBadProductGap_exp_bound line 126