Registry · Theorem
IV.T10
tau-effective
formalized
IV.T10 — Leading Exponent
Chowla-Selberg leading exponent at s=4 is -7 (= 1-2×4). Origin of ι_τ^(-7) in mass ratio formula. Proved by rfl.
Dependency Graph
Depends on (1)
Depended on by (1)
Lean Formalization
Module: TauLib.BookIV.Calibration.EpsteinZeta
Symbol: Tau.BookIV.Calibration.leading_exponent_is_neg7