OAI/NumberTheory/DirichletL/Descent/SecondMarkedEnergy.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseMoment.actualSecondChild_eraseline 15 - theorem
OAI.SevenEighths.InverseMoment.actualSecondChild_neg_frequencyline 18 - theorem
OAI.SevenEighths.InverseMoment.actual_second_marked_weighted_countline 25