OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/BernoulliWeight.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCofactorWeight.bernoulliWeight line 24
  2. lemma OAI.OrdinaryCofactorWeight.bernoulli_nonneg line 27
  3. lemma OAI.OrdinaryCofactorWeight.bernoulli_product line 35
  4. lemma OAI.OrdinaryCofactorWeight.generating_polynomial line 45
  5. lemma OAI.OrdinaryCofactorWeight.generating_le_exp line 54
  6. lemma OAI.OrdinaryCofactorWeight.beta_integral line 69
  7. lemma OAI.OrdinaryCofactorWeight.reciprocal_count_sq_le_beta line 86
  8. lemma OAI.OrdinaryCofactorWeight.exponential_beta_bound line 95
  9. theorem OAI.OrdinaryCofactorWeight.reciprocal_count_second_moment line 113