OAI/NumberTheory/DirichletL/PrimeRows/CoarseAmplitude.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbeHighRowFamily.coarsePrimeCost_image line 14
  2. lemma OAI.SevenEighths.ProbeHighRowFamily.prime_frequency_amplitude_le_one line 21
  3. def OAI.SevenEighths.ProbeHighRowFamily.contourArithmeticCost line 47
  4. lemma OAI.SevenEighths.ProbeHighRowFamily.contourArithmeticCost_nonneg line 50
  5. theorem OAI.SevenEighths.ProbeHighRowFamily.rowAmplitudeOnLines_buffered_polynomial line 53
  6. theorem OAI.SevenEighths.ProbeHighRowFamily.rowAmplitudeOnLines_first_polynomial line 80