OAI/NumberTheory/Ostmann/Construction/LogCellPNT.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Construction.tendsto_psi_nat_ratioline 9 - theorem
OAI.Ostmann.Construction.tendsto_psi_ratioline 31 - theorem
OAI.Ostmann.Construction.tendsto_theta_ratioline 44