OAI/NumberTheory/Ostmann/Characters/MixedFourier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Symmetries of the mixed Fourier bound

Conjugation and multiplication of the field argument by a unit preserve both the energy hypothesis and the mixed character/Fourier bound. These are the orientation changes used by the bottom pairs.

  1. def OAI.Ostmann.MixedFourierBound line 17
  2. theorem OAI.Ostmann.additiveFourier_conj line 21

    Distinct definitions of this name: OAI/NumberTheory/Ostmann/ZeroDensity/DensityFourierBounds.lean:68 (different declaration text). Qualify references as OAI.Ostmann.additiveFourier_conj@path.

  3. theorem OAI.Ostmann.MixedFourierBound.conj line 27
  4. theorem OAI.Ostmann.MixedFourierBound.unit_mul line 41
  5. theorem OAI.Ostmann.unit_mul_energy line 62