OAI/NumberTheory/Ostmann/QuadraticCenter/WalshTensorSplit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticCenter.flipSign line 8
  2. theorem OAI.Ostmann.QuadraticCenter.flipSign_involutive line 11
  3. def OAI.Ostmann.QuadraticCenter.flipSignEquiv line 20
  4. theorem OAI.Ostmann.QuadraticCenter.signMean_flip line 23
  5. theorem OAI.Ostmann.QuadraticCenter.sign_flipSign line 30
  6. theorem OAI.Ostmann.QuadraticCenter.sign_sq line 34
  7. theorem OAI.Ostmann.QuadraticCenter.walshCharacter_eq_prod line 36
  8. theorem OAI.Ostmann.QuadraticCenter.walshCharacter_empty line 41
  9. theorem OAI.Ostmann.QuadraticCenter.walshCharacter_insert line 45
  10. theorem OAI.Ostmann.QuadraticCenter.walshCharacter_flip_of_notMem line 50
  11. def OAI.Ostmann.QuadraticCenter.restrictedWalshPolynomial line 59
  12. def OAI.Ostmann.QuadraticCenter.restrictedWalshEnergy line 63
  13. theorem OAI.Ostmann.QuadraticCenter.restrictedWalshPolynomial_flip line 67
  14. theorem OAI.Ostmann.QuadraticCenter.restrictedWalshPolynomial_insert line 74
  15. theorem OAI.Ostmann.QuadraticCenter.restrictedWalshEnergy_insert line 87
  16. theorem OAI.Ostmann.QuadraticCenter.restrictedWalshEnergy_nonneg line 99