OAI/NumberTheory/DirichletL/Descent/FirstOriginalProfileLiveSource.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseMomentFirstOriginalProfile.refinedOuter line 14
2. def OAI.SevenEighths.InverseMomentFirstOriginalProfile.refinedSource line 18
3. lemma OAI.SevenEighths.InverseMomentFirstOriginalProfile.refinedSource_subset line 26
4. lemma OAI.SevenEighths.InverseMomentFirstOriginalProfile.original_weight_frequency line 34
5. theorem OAI.SevenEighths.InverseMomentFirstOriginalProfile.refined_source_radius line 41
6. def OAI.SevenEighths.InverseMomentFirstOriginalProfile.labelGate line 65
7. lemma OAI.SevenEighths.InverseMomentFirstOriginalProfile.refinedOuter_label line 69