OAI/NumberTheory/Ostmann/Characters/MixedExternalMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Elementary total-mass bounds for the original mixed external law

  1. theorem OAI.Ostmann.complexIntegerInterval_const line 12
  2. theorem OAI.Ostmann.complexPrimeInterval_const line 20
  3. theorem OAI.Ostmann.mixedExternalAverage_const line 28
  4. theorem OAI.Ostmann.integerLogCellMass_le_exp line 43
  5. theorem OAI.Ostmann.mixedExternalAverage_mass_bound line 54
  6. theorem OAI.Ostmann.mixedExternalAverage_re_nonneg line 83
  7. theorem OAI.Ostmann.mixedExternalAverage_re_mono line 93