OAI/NumberTheory/DirichletL/Inversion/InitialOriginalHeight.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseInitialOriginalHeight.child_eq_normTwistedline 12 - theorem
OAI.SevenEighths.InverseInitialOriginalHeight.child_supportline 17 - theorem
OAI.SevenEighths.InverseInitialOriginalHeight.child_smoothline 22 - theorem
OAI.SevenEighths.InverseInitialOriginalHeight.logSchwartz_childline 28