OAI/NumberTheory/TwoPoint/Halasz/HalaszLogOscillation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Calculus for the logarithmic phases in the sparse Dirichlet Gram kernel. The linear frequency is kept real for the later Poisson sum.

  1. def OAI.TwoPointCorrelations.halaszLogPhase line 13
  2. def OAI.TwoPointCorrelations.halaszLogSlope line 16
  3. def OAI.TwoPointCorrelations.halaszLogReciprocalDeriv line 18
  4. lemma OAI.TwoPointCorrelations.halasz_log_phase_norm line 21
  5. lemma OAI.TwoPointCorrelations.halasz_log_phase_deriv line 24
  6. lemma OAI.TwoPointCorrelations.halasz_log_reciprocal_deriv line 36
  7. lemma OAI.TwoPointCorrelations.halasz_log_phase_primitive_deriv line 48
  8. lemma OAI.TwoPointCorrelations.halasz_log_reciprocal_integral line 62