OAI/NumberTheory/DirichletL/Inversion/InitialHighFrequencyTailSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseInitialHighFrequencyTail.sourceKey line 15
2. def OAI.SevenEighths.InverseInitialHighFrequencyTail.sourcePoint line 18
3. theorem OAI.SevenEighths.InverseInitialHighFrequencyTail.sourcePoint_key line 22
4. def OAI.SevenEighths.InverseInitialHighFrequencyTail.sourceKeys line 26
5. def OAI.SevenEighths.InverseInitialHighFrequencyTail.sourceFrequencies line 28
6. theorem OAI.SevenEighths.InverseInitialHighFrequencyTail.mem_sourceFrequencies line 31
7. theorem OAI.SevenEighths.InverseInitialHighFrequencyTail.source_sum_fibers line 45
8. theorem OAI.SevenEighths.InverseInitialHighFrequencyTail.sourceKeys_card line 59