OAI/Combinatorics/Progressions/Estimates/PositiveRetainedDenominatorLog.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.positiveModerateLengthLog line 10
  2. def OAI.Erdos3.positiveModerateCoverLog line 13
  3. def OAI.Erdos3.positiveModerateSpectrumLog line 17
  4. def OAI.Erdos3.positiveModerateAccuracyLog line 20
  5. theorem OAI.Erdos3.positiveModerateLogs_nonneg line 24
  6. theorem OAI.Erdos3.positiveModerateLengthConstant_exp_bound line 39
  7. theorem OAI.Erdos3.positiveModerateCoverConstant_exp_bound line 50
  8. theorem OAI.Erdos3.positiveModerateSpectrumConstant_exp_bound line 74
  9. theorem OAI.Erdos3.positiveModerateAccuracyScale_exp_bound line 87
  10. def OAI.Erdos3.positiveRetainedBiasLog line 131
  11. def OAI.Erdos3.positiveSpectrumCardLog line 134
  12. def OAI.Erdos3.positiveRetainedFrequencyLog line 140
  13. theorem OAI.Erdos3.positiveRetainedLogs_nonneg line 144
  14. theorem OAI.Erdos3.positiveModerateRetainedBias_inverse_exp_bound line 159
  15. theorem OAI.Erdos3.positiveModerateSpectrumCardBudget_exp_bound line 172
  16. theorem OAI.Erdos3.positiveRetainedFrequencyBound_exp_bound line 208
  17. def OAI.Erdos3.positiveRetainedDenominatorLog line 246
  18. def OAI.Erdos3.positiveRetainedComplexityLog line 252
  19. theorem OAI.Erdos3.positiveRetainedDenominatorLog_nonneg line 257
  20. theorem OAI.Erdos3.positiveRetainedComplexityLog_bounds line 265
  21. theorem OAI.Erdos3.positiveRetainedDenominatorBound_exp_bound line 276
  22. theorem OAI.Erdos3.positiveRetainedComplexity_exp_bounds line 312