OAI/Combinatorics/Progressions/Estimates/InverseSqrtMoment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.inverse_max_le_inverse_sqrt_product line 12
  2. def OAI.Erdos3.unitInverseSqrt line 24
  3. theorem OAI.Erdos3.unitInverseSqrt_eq_rpow line 27
  4. theorem OAI.Erdos3.unitInverseSqrt_nonneg line 35
  5. theorem OAI.Erdos3.unitInverseSqrt_integrable line 38
  6. theorem OAI.Erdos3.unitInverseSqrt_mass line 44
  7. def OAI.Erdos3.unitBoxInverseSqrt line 52
  8. theorem OAI.Erdos3.unitBoxInverseSqrt_integrable line 54
  9. theorem OAI.Erdos3.unitBoxInverseSqrt_mass line 57
  10. theorem OAI.Erdos3.unitBoxInverseSqrt_eq line 62