OAI/NumberTheory/DirichletL/Moments/SecondCanonicalScalar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentSecondCanonicalScalar.normalizer line 16
  2. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalScalar.normalizer_pos line 19
  3. def OAI.SevenEighths.CenteredMomentSecondCanonicalScalar.retainedScalar line 26
  4. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalScalar.actual_retained_scalar_norm line 30
  5. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalScalar.original_partition_scalar line 40