OAI/NumberTheory/DirichletL/Descent/CanonicalRankExistenceInduction.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseMoment.RankReferenceCutoffsline 13 - def
OAI.SevenEighths.InverseMoment.RankReferenceThresholdsline 18 - theorem
OAI.SevenEighths.InverseMoment.rank_energy_exists_all_of_referencesline 23 - theorem
OAI.SevenEighths.InverseMoment.canonical_energy_exists_of_referencesline 43