OAI/NumberTheory/TwoPoint/Halasz/HalaszTriangleWeight.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A continuous compactly supported majorant of a dyadic interval. The adjoining affine pieces have exactly the integrals already estimated.

  1. def OAI.TwoPointCorrelations.halaszTriangleWeight line 12
  2. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_nonneg line 15
  3. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_le_two line 18
  4. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_left_zero line 25
  5. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_right_zero line 33
  6. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_left line 41
  7. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_right line 47
  8. lemma OAI.TwoPointCorrelations.halasz_triangle_weight_dyadic line 54
  9. def OAI.TwoPointCorrelations.halaszTriangleFunction line 64
  10. lemma OAI.TwoPointCorrelations.halasz_triangle_function_zero line 67
  11. lemma OAI.TwoPointCorrelations.halasz_triangle_function_continuous line 78
  12. lemma OAI.TwoPointCorrelations.halasz_triangle_function_compact line 93