OAI/NumberTheory/TwoPoint/Bounds/ComplexRawSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Numerical phase selection and the raw lower bound use the whole reciprocal mass. No phase or nonvanishing condition is imposed on individual primes.

  1. lemma OAI.TwoPointCorrelations.exists_weighted_phase_subset line 14
  2. lemma OAI.TwoPointCorrelations.weighted_dilated_correlation_comparison line 34
  3. lemma OAI.TwoPointCorrelations.raw_norm_lower_bound line 63