OAI/NumberTheory/DirichletL/Descent/ActualSecondProfile.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.InverseMoment.SecondProfileData line 13
2. def OAI.SevenEighths.InverseMoment.secondActualNorms line 27
3. lemma OAI.SevenEighths.InverseMoment.secondActualNorms_pos line 33
4. def OAI.SevenEighths.InverseMoment.secondActualCoefficient line 45
5. def OAI.SevenEighths.InverseMoment.actualSecondProfileRow line 58
6. theorem OAI.SevenEighths.InverseMoment.actualSecondProfileRow_eq_whole line 74