OAI/Combinatorics/Progressions/Probability/LowDensityAmplification.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.LowDensityThreshold line 12
  2. theorem OAI.Erdos3.exists_low_density_discount line 14
  3. theorem OAI.Erdos3.LowDensityThreshold.raw_target_lt_one line 27
  4. theorem OAI.Erdos3.LowDensityThreshold.mul_of_next line 33
  5. theorem OAI.Erdos3.LowDensityThreshold.of_next line 44
  6. theorem OAI.Erdos3.amplificationGain_low_density_parameters line 51
  7. theorem OAI.Erdos3.low_density_amplification_calls line 69
  8. theorem OAI.Erdos3.log_amplificationGain_le line 80
  9. theorem OAI.Erdos3.log_gain_at_selected_level_le line 93
  10. theorem OAI.Erdos3.eventually_low_density_at_selected_level line 100