OAI/Combinatorics/Progressions/Estimates/SmoothCoefficientSlice.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarCubeNormalizationThreshold line 12
  2. theorem OAI.Erdos3.scalarCubeNormalizationThreshold_spec line 18
  3. theorem OAI.Erdos3.scalarCube_weight_normalizer_of_threshold line 31
  4. def OAI.Erdos3.normalizedScalarCubeSourceOfThreshold line 49
  5. theorem OAI.Erdos3.scalarCubeNormalizationThreshold_le line 71
  6. theorem OAI.Erdos3.scalarCubeNormalizationThreshold_mul line 79
  7. theorem OAI.Erdos3.scalarCubeNormalizationThreshold_power_budget line 100
  8. structure OAI.Erdos3.SmoothCoefficientSlice line 123
  9. abbrev OAI.Erdos3.SmoothCoefficientSlice.Domain line 138
  10. def OAI.Erdos3.SmoothCoefficientSlice.sliceWeight line 140
  11. theorem OAI.Erdos3.SmoothCoefficientSlice.sliceWeight_nonneg line 142
  12. def OAI.Erdos3.SmoothCoefficientSlice.law line 144
  13. def OAI.Erdos3.SmoothCoefficientSlice.finiteSlice line 147
  14. theorem OAI.Erdos3.SmoothCoefficientSlice.affine_abs_le line 154
  15. def OAI.Erdos3.SmoothCoefficientSlice.longNormalizer line 163
  16. theorem OAI.Erdos3.SmoothCoefficientSlice.longNormalizer_bounds line 169
  17. theorem OAI.Erdos3.SmoothCoefficientSlice.longNormalizer_eq_expect line 175
  18. theorem OAI.Erdos3.SmoothCoefficientSlice.long_total_pos line 188
  19. def OAI.Erdos3.SmoothCoefficientSlice.normalized line 195
  20. theorem OAI.Erdos3.SmoothCoefficientSlice.normalized_coefficientDensity line 201
  21. theorem OAI.Erdos3.SmoothCoefficientSlice.normalized_coefficientWeights line 205