OAI/Combinatorics/Progressions/Estimates/InactiveShortLogBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.profileWidthFactor_le line 12
  2. theorem OAI.Erdos3.normalizedCoefficientCoordinates_lipschitz line 20
  3. def OAI.Erdos3.affineProductProfileLip line 38
  4. theorem OAI.Erdos3.affineProductProfile_lipschitz line 41
  5. theorem OAI.Erdos3.affineProductProfile_cap line 65
  6. theorem OAI.Erdos3.pow_le_exp_mul_of_le_exp line 81
  7. theorem OAI.Erdos3.mixedInterpolation_constants_exp_bounds line 88
  8. def OAI.Erdos3.coefficientReplacementErrorLog line 132
  9. theorem OAI.Erdos3.coefficientReplacementError_small line 135
  10. def OAI.Erdos3.inactiveNaturalShortScale line 186
  11. def OAI.Erdos3.inactiveShortScaleLog line 188
  12. def OAI.Erdos3.inactiveShortCapLog line 191
  13. def OAI.Erdos3.inactiveShortLipschitzLog line 194
  14. theorem OAI.Erdos3.inactiveShortLogs_nonneg line 197
  15. theorem OAI.Erdos3.inactiveNaturalShortScale_exp_bound line 203
  16. theorem OAI.Erdos3.inactiveNaturalShortResources_exp_bounds line 223