OAI/NumberTheory/DirichletL/Descent/CanonicalRankExistenceData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseMoment.CompletePoolRankMoments line 15
2. def OAI.SevenEighths.InverseMoment.rankRowCap line 27
3. def OAI.SevenEighths.InverseMoment.rankTotalCap line 29
4. def OAI.SevenEighths.InverseMoment.rankMargin line 31
5. def OAI.SevenEighths.InverseMoment.rankLoss line 33
6. def OAI.SevenEighths.InverseMoment.RankEnergyExists line 35
7. theorem OAI.SevenEighths.InverseMoment.rank_energy_exists_zero line 51
8. theorem OAI.SevenEighths.InverseMoment.actual_rank_successor_caps line 65