OAI/NumberTheory/Ostmann/Characters/MixedExternalAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The original root, prime and integer average as one finite positive law

  1. abbrev OAI.Ostmann.MixedExternalPoint line 12
  2. def OAI.Ostmann.mixedExternalPrior line 16
  3. def OAI.Ostmann.mixedExternalAverage line 23
  4. theorem OAI.Ostmann.mixedExternalPrior_nonneg line 30
  5. theorem OAI.Ostmann.mixedExternalAverage_finite line 39
  6. theorem OAI.Ostmann.mixedExternalAverage_star line 77
  7. theorem OAI.Ostmann.mixedExternalAverage_correlation_le line 84