OAI/NumberTheory/DirichletL/Descent/TripleMass.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseMoment.tripleDivisorWeightline 11 - lemma
OAI.SevenEighths.InverseMoment.tripleDivisorWeight_nonnegline 16 - theorem
OAI.SevenEighths.InverseMoment.ideal_divisor_power_smallline 19 - theorem
OAI.SevenEighths.InverseMoment.tripleDivisorWeight_smallline 40 - theorem
OAI.SevenEighths.InverseMoment.outerTriple_cardline 63 - theorem
OAI.SevenEighths.InverseMoment.triple_normalized_massline 79