OAI/NumberTheory/Ostmann/Characters/RademacherMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact moments of the Boolean monomials

  1. def OAI.Ostmann.monomialOccurrence line 11
  2. theorem OAI.Ostmann.rademacherMonomial_univ line 15
  3. theorem OAI.Ostmann.rademacherMonomial_product line 20
  4. theorem OAI.Ostmann.bool_sign_power_sum line 32
  5. theorem OAI.Ostmann.rademacher_product_average line 38
  6. theorem OAI.Ostmann.rademacher_even_moment line 56