OAI/NumberTheory/DirichletL/Descent/FullProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseMoment.rootSchwartz line 10
2. theorem OAI.SevenEighths.InverseMoment.rootSchwartz_apply line 14
3. theorem OAI.SevenEighths.InverseMoment.full_source_profile_common_measure line 18
4. def OAI.SevenEighths.InverseMoment.firstRootSchwartz line 58
5. theorem OAI.SevenEighths.InverseMoment.first_full_profile_common_measure line 65
6. def OAI.SevenEighths.InverseMoment.secondRootSchwartz line 94
7. theorem OAI.SevenEighths.InverseMoment.second_full_profile_common_measure line 101