OAI/Combinatorics/Progressions/Probability/RelativeSourceDensityParameter.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.densityParameter line 12
  2. theorem OAI.Erdos3.densityParameter_ge_two line 14
  3. theorem OAI.Erdos3.densityParameter_drop line 16
  4. theorem OAI.Erdos3.selected_amplification_log_gain line 32
  5. theorem OAI.Erdos3.density_le_exp_sub_parameter line 55
  6. theorem OAI.Erdos3.density_parameter_ge_of_invariant_failure line 65
  7. def OAI.Erdos3.intervalIndicator line 92
  8. def OAI.Erdos3.intervalDensity line 94
  9. theorem OAI.Erdos3.intervalIndicator_mem_Icc line 96
  10. theorem OAI.Erdos3.mean_intervalIndicator line 101
  11. theorem OAI.Erdos3.intervalDensity_pos line 116
  12. theorem OAI.Erdos3.intervalDensity_le_one line 120
  13. def OAI.Erdos3.progressionPreimage line 125
  14. theorem OAI.Erdos3.progressionPreimage_subset line 128
  15. theorem OAI.Erdos3.APFree.progressionPreimage line 131
  16. theorem OAI.Erdos3.mean_progression_indicator line 137
  17. theorem OAI.Erdos3.intervalDensity_pos_iff line 146
  18. theorem OAI.Erdos3.eventually_sublinear_drop_room line 165
  19. theorem OAI.Erdos3.exists_selected_density_drop line 176
  20. theorem OAI.Erdos3.FixedDensity.exists_naturalAP_of_cyclicAPVal_shortInterval line 205
  21. def OAI.Erdos3.cyclicIntervalSet line 261
  22. theorem OAI.Erdos3.cyclicIntervalSet_card line 265
  23. theorem OAI.Erdos3.fixed_density_hasAP line 283
  24. theorem OAI.Erdos3.exp_neg_le_density_of_parameter_le line 359
  25. theorem OAI.Erdos3.fixed_density_terminal line 367
  26. structure OAI.Erdos3.APFreeInterval line 399
  27. def OAI.Erdos3.APFreeInterval.density line 411
  28. def OAI.Erdos3.APFreeInterval.parameter line 413
  29. theorem OAI.Erdos3.APFreeInterval.density_pos line 415
  30. theorem OAI.Erdos3.APFreeInterval.parameter_ge_two line 418
  31. def OAI.Erdos3.APFreeInterval.reindex line 420
  32. theorem OAI.Erdos3.no_interval_invariant_of_descent line 431
  33. theorem OAI.Erdos3.densityParameter_eq_log_of_two_lt line 461
  34. theorem OAI.Erdos3.exp_neg_densityParameter_eq_half line 468
  35. theorem OAI.Erdos3.APFreeInterval.exp_neg_parameter_eq_half line 477