OAI/Combinatorics/Progressions/Geometry/UnitBoxAmplitude.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.positiveUnitBox line 14
  2. theorem OAI.Erdos3.positiveUnitBox_measurable line 16
  3. def OAI.Erdos3.unitBoxMeasure line 19
  4. instance OAI.Erdos3.unitBoxMeasure_probability line 22
  5. theorem OAI.Erdos3.unitBoxMeasure_ae line 27
  6. theorem OAI.Erdos3.unitBoxInverseSqrt_indicator line 31
  7. theorem OAI.Erdos3.unitBox_inverse_sqrt_integrable line 46
  8. theorem OAI.Erdos3.unitBox_inverse_sqrt_mass line 52
  9. def OAI.Erdos3.pairedAmplitude line 58
  10. theorem OAI.Erdos3.pairedAmplitude_continuous line 61
  11. theorem OAI.Erdos3.pairedAmplitude_pos_ae line 65
  12. theorem OAI.Erdos3.pairedAmplitude_inverse_bound line 70
  13. theorem OAI.Erdos3.pairedAmplitude_inverse_integrable line 78
  14. theorem OAI.Erdos3.pairedAmplitude_inverse_integral_le line 89