OAI/NumberTheory/Ostmann/Arithmetic/HarmonicHistorySupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic support bound under the original prime priors

The residue modulus is allowed to depend on the entire fixed frequency history. Only the prime samples are averaged, with their original priors.

  1. def OAI.Ostmann.harmonicHistorySupportSum line 16
  2. theorem OAI.Ostmann.harmonic_history_support_le line 28