OAI/Combinatorics/Progressions/Lattices/AveragedAffineLogMixedGrid.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.idealOutputLog line 12
  2. theorem OAI.Erdos3.idealOutputLog_nonneg line 14
  3. theorem OAI.Erdos3.idealOutputBound_le_exp line 17
  4. def OAI.Erdos3.commonAffineOutputLog line 38
  5. theorem OAI.Erdos3.commonAffineOutputLog_nonneg line 43
  6. theorem OAI.Erdos3.commonAffineOutputLog_radius line 52
  7. theorem OAI.Erdos3.commonAffineOutputLog_ideal line 69
  8. theorem OAI.Erdos3.averagedAffine_log_density_data line 93
  9. def OAI.Erdos3.affineGridCommonLog line 167
  10. def OAI.Erdos3.affineMixedGridLog line 173
  11. theorem OAI.Erdos3.affineGridCommonLog_nonneg line 178
  12. theorem OAI.Erdos3.affineMixedGridLog_nonneg line 188
  13. theorem OAI.Erdos3.affineMixedGridAllowance_le_exp line 196
  14. def OAI.Erdos3.affineMixedGridAccuracy line 221
  15. theorem OAI.Erdos3.affineMixedGridAccuracy_spec line 225
  16. theorem OAI.Erdos3.affineMixedGridAccuracy_inverse_le_exp line 235
  17. theorem OAI.Erdos3.averagedAffine_log_mixed_grid_error line 263