OAI/NumberTheory/TwoPoint/Fourier/MinorArcKernelSymmetry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positivity and reflection symmetry of the resonant-safe geometric kernel.

  1. lemma OAI.TwoPointCorrelations.minor_arc_geometric_nonneg line 12
  2. lemma OAI.TwoPointCorrelations.minor_arc_character_neg line 19
  3. lemma OAI.TwoPointCorrelations.minor_arc_geometric_neg line 27
  4. lemma OAI.TwoPointCorrelations.minor_arc_geometric_natAbs line 45