OAI/NumberTheory/Ostmann/ZeroDensity/GiantHaarDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact Haar residue factors inside the real giant integral

  1. def OAI.Ostmann.pageGiantWeight line 11
  2. def OAI.Ostmann.correctedPrimePairAverage line 15
  3. def OAI.Ostmann.correctedMixedPairAverage line 22
  4. theorem OAI.Ostmann.selectedPrimeLogDensity_page line 28
  5. theorem OAI.Ostmann.prime_pair_density_haar line 34
  6. theorem OAI.Ostmann.mixed_pair_density_haar line 48