OAI/NumberTheory/DirichletL/Moments/PositiveSummability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentPositiveSummability.plain_finite_norm line 17
  2. lemma OAI.SevenEighths.CenteredMomentPositiveSummability.slot_finite_norm line 37
  3. lemma OAI.SevenEighths.CenteredMomentPositiveSummability.bounded_radial_summable line 43
  4. lemma OAI.SevenEighths.CenteredMomentPositiveSummability.product_bounded line 58
  5. theorem OAI.SevenEighths.CenteredMomentPositiveSummability.retained_positive_summable line 77
  6. theorem OAI.SevenEighths.CenteredMomentPositiveSummability.allocated_positive_summable line 92