OAI/Combinatorics/Progressions/Estimates/CanonicalScalarSourceEnvelope.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.principalIntervalLength line 13
  2. def OAI.Erdos3.principalIntervalWeight line 16
  3. theorem OAI.Erdos3.principalIntervalLength_pos line 25
  4. theorem OAI.Erdos3.principalIntervalLength_bounds line 30
  5. theorem OAI.Erdos3.principalIntervalLength_support line 41
  6. theorem OAI.Erdos3.principalIntervalWeight_grid line 54
  7. theorem OAI.Erdos3.principalIntervalWeight_range line 71
  8. theorem OAI.Erdos3.principalIntervalWeight_lipschitz line 91
  9. theorem OAI.Erdos3.paddedResidueDensityCap_mono line 134
  10. theorem OAI.Erdos3.ScalarCubePrimitiveBudget.mono line 139
  11. def OAI.Erdos3.scalarCubePrimitiveEnvelope line 146
  12. theorem OAI.Erdos3.scalarCubePrimitiveBudget_of_raw_bounds line 154
  13. theorem OAI.Erdos3.scalarCubePrimitiveEnvelope_nonneg line 217
  14. theorem OAI.Erdos3.scalarCubePrimitiveEnvelope_mono line 223
  15. theorem OAI.Erdos3.paddedResidueDensityCap_scale line 233
  16. theorem OAI.Erdos3.scalarCubePrimitiveEnvelope_split line 239
  17. theorem OAI.Erdos3.scalarCubePrimitiveEnvelope_le_scaled line 247
  18. theorem OAI.Erdos3.scalarCubePrimitiveEnvelope_eq_of_card line 273
  19. def OAI.Erdos3.normalizedUniformCubeSource line 291
  20. theorem OAI.Erdos3.normalizedUniformCubeSource_mean line 311
  21. theorem OAI.Erdos3.normalizedUniformCubeSource_primitive line 321
  22. theorem OAI.Erdos3.normalizedUniformCubeSource_translated_mean line 328
  23. def OAI.Erdos3.normalizedProgressionCubeSource line 342
  24. theorem OAI.Erdos3.normalizedProgressionCubeSource_mean line 348
  25. theorem OAI.Erdos3.normalizedProgressionCubeSource_primitive line 358
  26. def OAI.Erdos3.principalNormalizedSource line 374
  27. theorem OAI.Erdos3.principalNormalizedSource_parameters line 390
  28. theorem OAI.Erdos3.principalNormalizedSource_law line 397
  29. theorem OAI.Erdos3.principalNormalizedSource_primitive line 409
  30. def OAI.Erdos3.scalarSourceTransitionBound line 425
  31. theorem OAI.Erdos3.scalarSourceTransitionBound_spec line 428
  32. def OAI.Erdos3.canonicalScalarSourceDegree line 433
  33. def OAI.Erdos3.canonicalScalarSourceConstant line 435
  34. theorem OAI.Erdos3.canonicalScalarSourceConstant_bounds line 439
  35. def OAI.Erdos3.canonicalScalarSourceEnvelope line 459
  36. def OAI.Erdos3.canonicalScalarSourceLog line 462
  37. theorem OAI.Erdos3.canonicalScalarSourceConstant_le_envelope line 465
  38. theorem OAI.Erdos3.canonicalScalarSourceEnvelope_bounds line 472
  39. theorem OAI.Erdos3.canonicalScalarSourceLog_bounds line 502
  40. theorem OAI.Erdos3.canonicalScalarSourceEnvelope_le_exp line 510