OAI/Combinatorics/Progressions/Polynomial/ModeLogPolynomials.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.modeProfileLogPolynomial line 12
  2. def OAI.Erdos3.modeBiasLogPolynomial line 14
  3. def OAI.Erdos3.modeShrinkLogPolynomial line 17
  4. def OAI.Erdos3.modeSideLogPolynomial line 20
  5. def OAI.Erdos3.modeRankLogPolynomial line 23
  6. theorem OAI.Erdos3.modeProfileLogPolynomial_eval line 29
  7. theorem OAI.Erdos3.modeBiasLogPolynomial_eval line 33
  8. theorem OAI.Erdos3.modeShrinkLogPolynomial_eval line 37
  9. theorem OAI.Erdos3.modeSideLogPolynomial_eval line 41
  10. theorem OAI.Erdos3.modeRankLogPolynomial_eval line 46
  11. theorem OAI.Erdos3.exists_mode_threshold_exp_budget line 51