OAI/Combinatorics/Progressions/Dynamics/JointPivotProfileBudget.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.normalizedFiberErrorConstant_le_exp line 12
  2. theorem OAI.Erdos3.coefficientComparisonConstant_le_exp line 65
  3. def OAI.Erdos3.affineProfileLogBound line 91
  4. theorem OAI.Erdos3.affineProfileLogBound_nonneg line 94
  5. theorem OAI.Erdos3.profileWidthPower_le_exp line 99
  6. theorem OAI.Erdos3.affineProductProfileLip_le_exp line 105
  7. theorem OAI.Erdos3.affineProductProfile_cap_le_exp line 122
  8. def OAI.Erdos3.affineCoefficientCommonBudget line 130
  9. theorem OAI.Erdos3.affineCoefficientCommonBudget_nonneg line 133
  10. theorem OAI.Erdos3.affineCoefficientCommonBudget_bounds line 138
  11. theorem OAI.Erdos3.affineCoefficientConstants_le_exp line 149
  12. theorem OAI.Erdos3.inverseJacobian_le_exp line 190
  13. theorem OAI.Erdos3.pivotKernelCap_le_exp line 202
  14. theorem OAI.Erdos3.pivotKernelLip_le_exp line 221
  15. def OAI.Erdos3.pivotProfileLog line 233
  16. theorem OAI.Erdos3.pivotProfileLog_nonneg line 236
  17. theorem OAI.Erdos3.scaledWidth_inverse_le_exp line 242
  18. theorem OAI.Erdos3.pivotProfile_regularity_le_exp line 250
  19. def OAI.Erdos3.jointPivotProfileLog line 287
  20. theorem OAI.Erdos3.jointPivotProfileLog_nonneg line 291
  21. theorem OAI.Erdos3.pivotProfileLog_le_joint line 296
  22. theorem OAI.Erdos3.jointPivotProfile_regularity line 304
  23. theorem OAI.Erdos3.jointDensityLip_le_exp line 326