OAI/NumberTheory/Ostmann/QuadraticCenter/WalshMoments.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticCenter.sign line 8
  2. theorem OAI.Ostmann.QuadraticCenter.sign_false line 10
  3. theorem OAI.Ostmann.QuadraticCenter.sign_true line 11
  4. def OAI.Ostmann.QuadraticCenter.signMonomial line 13
  5. def OAI.Ostmann.QuadraticCenter.signMean line 16
  6. theorem OAI.Ostmann.QuadraticCenter.sign_pow_sum line 19
  7. theorem OAI.Ostmann.QuadraticCenter.signMonomial_sum line 28
  8. theorem OAI.Ostmann.QuadraticCenter.signMonomial_mean line 44
  9. theorem OAI.Ostmann.QuadraticCenter.signMonomial_add line 52
  10. theorem OAI.Ostmann.QuadraticCenter.signMonomial_sum_exponents line 57
  11. theorem OAI.Ostmann.QuadraticCenter.signMean_power_sum line 64
  12. theorem OAI.Ostmann.QuadraticCenter.signMean_const_mul line 93
  13. theorem OAI.Ostmann.QuadraticCenter.signMean_sum line 99
  14. def OAI.Ostmann.QuadraticCenter.walshCharacter line 105
  15. theorem OAI.Ostmann.QuadraticCenter.walshCharacter_orthogonality line 109
  16. theorem OAI.Ostmann.QuadraticCenter.walsh_sum_sq_mean line 127