OAI/NumberTheory/Jacobsthal/Harmonic/FourierDerivative.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.AdditiveLargeSieve.monomial line 17
  2. def OAI.Erdos970.AdditiveLargeSieve.polynomial line 18
  3. theorem OAI.Erdos970.AdditiveLargeSieve.monomial_continuous line 21
  4. theorem OAI.Erdos970.AdditiveLargeSieve.polynomial_continuous line 24
  5. theorem OAI.Erdos970.AdditiveLargeSieve.unit_monomial_integral line 29
  6. theorem OAI.Erdos970.AdditiveLargeSieve.monomial_conj_mul line 35
  7. theorem OAI.Erdos970.AdditiveLargeSieve.polynomial_square_expansion line 41
  8. theorem OAI.Erdos970.AdditiveLargeSieve.polynomial_energy line 53
  9. theorem OAI.Erdos970.AdditiveLargeSieve.polynomial_energy_two line 74
  10. def OAI.Erdos970.AdditiveLargeSieve.derivativeCoefficients line 96
  11. theorem OAI.Erdos970.AdditiveLargeSieve.polynomial_hasDerivAt line 99
  12. theorem OAI.Erdos970.AdditiveLargeSieve.derivative_coefficient_norm line 109
  13. theorem OAI.Erdos970.AdditiveLargeSieve.derivative_energy_le line 113
  14. theorem OAI.Erdos970.AdditiveLargeSieve.norm_square_derivative_bound line 130
  15. theorem OAI.Erdos970.AdditiveLargeSieve.separated_polynomial_bound line 140