OAI/NumberTheory/DirichletL/Descent/CanonicalRankExistence.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseMoment.actual_rank_reference_cutoffsline 11 - theorem
OAI.SevenEighths.InverseMoment.actual_rank_reference_thresholdsline 17 - theorem
OAI.SevenEighths.InverseMoment.canonical_rank_energy_existsline 21 - theorem
OAI.SevenEighths.InverseMoment.canonical_marked_energy_existsline 32