OAI/NumberTheory/DirichletL/Descent/SecondGenerator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseMoment.secondUnitFrequency line 12
2. lemma OAI.SevenEighths.InverseMoment.secondUnitFrequency_injective line 14
3. lemma OAI.SevenEighths.InverseMoment.secondUnitFrequency_norm line 18
4. lemma OAI.SevenEighths.InverseMoment.secondUnitFrequency_neg line 23
5. theorem OAI.SevenEighths.InverseMoment.secondCanonical_generator_transport line 32
6. theorem OAI.SevenEighths.InverseMoment.secondCanonical_row_norm line 49
7. theorem OAI.SevenEighths.InverseMoment.exists_second_generator_sectors line 64