OAI/Combinatorics/Progressions/Sampling/PositiveGridFamily.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.positiveGrid_normalization_bound line 13
  2. theorem OAI.Erdos3.positiveGrid_compression_errors line 26
  3. theorem OAI.Erdos3.exists_positiveGrid_base_budget line 63
  4. theorem OAI.Erdos3.exists_positiveGrid_slack line 85
  5. theorem OAI.Erdos3.positiveGrid_power_gap line 107
  6. abbrev OAI.Erdos3.PositiveGridVertex line 130
  7. abbrev OAI.Erdos3.PositiveGridShifts line 132
  8. def OAI.Erdos3.positiveGridVolume line 134
  9. def OAI.Erdos3.positiveGridProduct line 136
  10. def OAI.Erdos3.positiveGridMean line 140
  11. theorem OAI.Erdos3.positiveGridVertex_card line 144
  12. theorem OAI.Erdos3.positiveGridVolume_succ line 148
  13. theorem OAI.Erdos3.positiveGridVolume_pos line 152
  14. theorem OAI.Erdos3.positiveGridVolume_le line 155
  15. theorem OAI.Erdos3.positiveGridProduct_nonneg line 162
  16. theorem OAI.Erdos3.positiveGridProduct_le_exp line 166
  17. theorem OAI.Erdos3.prod_dependent_fin_cons line 186
  18. def OAI.Erdos3.positiveGridFiber line 197
  19. theorem OAI.Erdos3.positiveGridProduct_cons line 202
  20. theorem OAI.Erdos3.positiveGridMean_first_axis line 223
  21. theorem OAI.Erdos3.positiveGridMean_fiber line 230
  22. theorem OAI.Erdos3.rootGrid_product line 247
  23. theorem OAI.Erdos3.rootGrid_mean line 256
  24. theorem OAI.Erdos3.scaledRootGrid_mean line 269
  25. theorem OAI.Erdos3.positiveGridProduct_zero line 298
  26. theorem OAI.Erdos3.positiveGridProduct_one_axis line 305
  27. theorem OAI.Erdos3.positiveGridMean_one_axis line 313
  28. theorem OAI.Erdos3.positiveGridMean_one_axis_le line 321
  29. def OAI.Erdos3.PositiveGridEstimate line 346
  30. theorem OAI.Erdos3.positiveGridMean_one_axis_slack line 356
  31. theorem OAI.Erdos3.exists_positiveGridEstimate_zero line 367
  32. theorem OAI.Erdos3.exists_positiveGrid_compression_bound line 390
  33. theorem OAI.Erdos3.exists_positiveGridEstimate_step line 448
  34. theorem OAI.Erdos3.exists_positiveGridEstimate line 562
  35. theorem OAI.Erdos3.exists_positiveGrid_counting line 581
  36. theorem OAI.Erdos3.CyclicNiltestUpperComparison.of_pointwise line 658
  37. theorem OAI.Erdos3.exists_positiveGrid_family_counting line 667