OAI/Combinatorics/Progressions/Estimates/UniformScaledRetainedLogBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.uniformRetainedBiasLog line 9
  2. def OAI.Erdos3.uniformSpectrumCardLog line 13
  3. def OAI.Erdos3.uniformRetainedFrequencyLog line 18
  4. def OAI.Erdos3.uniformRetainedDenominatorLog line 23
  5. theorem OAI.Erdos3.uniformRetainedLogs_nonneg line 30
  6. theorem OAI.Erdos3.uniformBlockRetainedBias_inverse_exp_bound line 50
  7. theorem OAI.Erdos3.uniformSpectrumCardBound_exp_bound line 62
  8. theorem OAI.Erdos3.uniformBlockSpectrumCardBudget_exp_bound line 77
  9. theorem OAI.Erdos3.uniformRetainedFrequency_exp_bound line 87
  10. theorem OAI.Erdos3.uniformCharacterDenominatorBound_exp_bound line 110
  11. theorem OAI.Erdos3.uniformScaledRetainedFrequencyBound_le line 164
  12. theorem OAI.Erdos3.uniformScaledRetainedDenominatorBound_le line 176
  13. theorem OAI.Erdos3.uniformScaledRetained_exp_bounds line 200