OAI/NumberTheory/DirichletL/Moments/PlainChildEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentPlainChildEnergy.leftColumn_eq_rowPolynomial line 13
  2. theorem OAI.SevenEighths.CenteredMomentPlainChildEnergy.rightColumn_eq_star_rowPolynomial line 23
  3. theorem OAI.SevenEighths.CenteredMomentPlainChildEnergy.whole_kernel_plain_child_bound line 33