OAI/NumberTheory/DirichletL/Descent/CanonicalRankFamilyGates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.actual_rank_family_period line 14
2. theorem OAI.SevenEighths.InverseMoment.actual_rank_family_gates line 27
3. theorem OAI.SevenEighths.InverseMoment.actual_rank_norm_width line 34
4. theorem OAI.SevenEighths.InverseMoment.actual_rank_state_gates line 40
5. theorem OAI.SevenEighths.InverseMoment.canonical_rank_subslots line 59
6. theorem OAI.SevenEighths.InverseMoment.canonical_rank_subslot_product line 71
7. theorem OAI.SevenEighths.InverseMoment.canonical_rank_subslot_cap line 79